Loogle!

Result

Found 346 declarations whose name contains "baseChange". Of these, only the first 200 are shown.

Submodule.baseChange 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
{R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Submodule A (TensorProduct R A M)
Submodule.baseChange_bot 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
{R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] : Submodule.baseChange A ⊥ = ⊥
Submodule.baseChange_top 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
{R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] : Submodule.baseChange A ⊤ = ⊤
Submodule.tmul_mem_baseChange_of_mem 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
{R : Type u_1} {M : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] {p : Submodule R M} (a : A) {m : M} (hm : m ∈ p) : a ⊗ₜ[R] m ∈ Submodule.baseChange A p
TensorProduct.AlgebraTensorModule.cancelBaseChange 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
(R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [Module B M] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] [AddCommMonoid N] [Module R N] [Algebra A B] [IsScalarTower A B M] : TensorProduct A M (TensorProduct R A N) ≃ₗ[B] TensorProduct R M N
TensorProduct.AlgebraTensorModule.distribBaseChange 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
(R : Type uR) (A : Type uA) (M : Type uM) (N : Type uN) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : TensorProduct R A (TensorProduct R M N) ≃ₗ[A] TensorProduct A (TensorProduct R A M) (TensorProduct R A N)
Submodule.baseChange.eq_1 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
{R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Submodule.baseChange A p = Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) p)
Submodule.baseChange_span 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
{R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (s : Set M) : Submodule.baseChange A (Submodule.span R s) = Submodule.span A (⇑((TensorProduct.mk R A M) 1) '' s)
TensorProduct.AlgebraTensorModule.cancelBaseChange_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
(R : Type uR) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [Module B M] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] [AddCommMonoid N] [Module R N] [Algebra A B] [IsScalarTower A B M] (m : M) (n : N) (a : A) : (TensorProduct.AlgebraTensorModule.cancelBaseChange R A B M N) (m ⊗ₜ[A] a ⊗ₜ[R] n) = (a • m) ⊗ₜ[R] n
TensorProduct.AlgebraTensorModule.cancelBaseChange_symm_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
(R : Type uR) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [Module B M] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] [AddCommMonoid N] [Module R N] [Algebra A B] [IsScalarTower A B M] (m : M) (n : N) : (TensorProduct.AlgebraTensorModule.cancelBaseChange R A B M N).symm (m ⊗ₜ[R] n) = m ⊗ₜ[A] 1 ⊗ₜ[R] n
TensorProduct.AlgebraTensorModule.lTensor_comp_cancelBaseChange 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
(R : Type uR) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} {Q : Type uQ} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [Module B M] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] [AddCommMonoid N] [Module R N] [AddCommMonoid Q] [Module R Q] [Algebra A B] [IsScalarTower A B M] (f : N →ₗ[R] Q) : (TensorProduct.AlgebraTensorModule.lTensor B M) f ∘ₗ ↑(TensorProduct.AlgebraTensorModule.cancelBaseChange R A B M N) = ↑(TensorProduct.AlgebraTensorModule.cancelBaseChange R A B M Q) ∘ₗ (TensorProduct.AlgebraTensorModule.lTensor B M) ((TensorProduct.AlgebraTensorModule.lTensor A A) f)
Basis.baseChange 📋 Mathlib.LinearAlgebra.TensorProduct.Basis
{R : Type u_1} {M : Type u_3} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_7) [Semiring S] [Algebra R S] (b : Basis ι R M) : Basis ι S (TensorProduct R S M)
Basis.baseChange.eq_1 📋 Mathlib.LinearAlgebra.TensorProduct.Basis
{R : Type u_1} {M : Type u_3} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_7) [Semiring S] [Algebra R S] (b : Basis ι R M) : Basis.baseChange S b = ((Basis.singleton Unit S).tensorProduct b).reindex (Equiv.punitProd ι)
Basis.baseChange_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basis
{R : Type u_1} {M : Type u_3} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_7) [Semiring S] [Algebra R S] (b : Basis ι R M) (i : ι) : (Basis.baseChange S b) i = 1 ⊗ₜ[R] b i
Basis.baseChange_repr_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Basis
{R : Type u_1} {M : Type u_3} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_7) [Semiring S] [Algebra R S] (b : Basis ι R M) (x : S) (y : M) (i : ι) : ((Basis.baseChange S b).repr (x ⊗ₜ[R] y)) i = (b.repr y) i • x
LinearMap.baseChange 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type u_1} (A : Type u_2) {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) : TensorProduct R A M →ₗ[A] TensorProduct R A N
LinearEquiv.baseChange 📋 Mathlib.RingTheory.TensorProduct.Basic
(R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (e : M ≃ₗ[R] N) : TensorProduct R A M ≃ₗ[A] TensorProduct R A N
LinearMap.baseChange_id 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] : LinearMap.baseChange A LinearMap.id = LinearMap.id
LinearMap.liftBaseChange 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type u_1} {M : Type u_2} {N : Type u_3} (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] (l : M →ₗ[R] N) : TensorProduct R A M →ₗ[A] N
LinearMap.baseChange_tmul 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) (a : A) (x : M) : (LinearMap.baseChange A f) (a ⊗ₜ[R] x) = a ⊗ₜ[R] f x
LinearMap.baseChange_comp 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} {P : Type u_6} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) : LinearMap.baseChange A (g ∘ₗ f) = LinearMap.baseChange A g ∘ₗ LinearMap.baseChange A f
Module.End.baseChangeHom 📋 Mathlib.RingTheory.TensorProduct.Basic
(R : Type u_1) (A : Type u_2) (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] : Module.End R M →ₐ[R] Module.End A (TensorProduct R A M)
LinearMap.baseChange_one 📋 Mathlib.RingTheory.TensorProduct.Basic
(R : Type u_1) {A : Type u_2} (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] : LinearMap.baseChange A 1 = 1
LinearMap.liftBaseChange_one_tmul 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type u_1} {M : Type u_2} {N : Type u_3} (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] (l : M →ₗ[R] N) (y : M) : (LinearMap.liftBaseChange A l) (1 ⊗ₜ[R] y) = l y
LinearMap.baseChange_zero 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : LinearMap.baseChange A 0 = 0
LinearMap.liftBaseChange_tmul 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type u_1} {M : Type u_2} {N : Type u_3} (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] (l : M →ₗ[R] N) (x : A) (y : M) : (LinearMap.liftBaseChange A l) (x ⊗ₜ[R] y) = x • l y
Algebra.TensorProduct.cancelBaseChange 📋 Mathlib.RingTheory.TensorProduct.Basic
(R : Type uR) (S : Type uS) [CommSemiring R] [CommSemiring S] [Algebra R S] (T : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring T] [CommSemiring A] [CommSemiring B] [Algebra R T] [Algebra R A] [Algebra R B] [Algebra T A] [IsScalarTower R T A] [Algebra S A] [IsScalarTower R S A] [Algebra S T] [IsScalarTower S T A] : TensorProduct S A (TensorProduct R S B) ≃ₐ[T] TensorProduct R A B
LinearMap.baseChangeHom 📋 Mathlib.RingTheory.TensorProduct.Basic
(R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : (M →ₗ[R] N) →ₗ[R] TensorProduct R A M →ₗ[A] TensorProduct R A N
LinearMap.baseChange_eq_ltensor 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) : ⇑(LinearMap.baseChange A f) = ⇑(LinearMap.lTensor A f)
LinearMap.liftBaseChangeEquiv 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type u_1} {M : Type u_2} {N : Type u_3} (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] : (M →ₗ[R] N) ≃ₗ[A] TensorProduct R A M →ₗ[A] N
LinearMap.baseChange_neg 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : LinearMap.baseChange A (-f) = -LinearMap.baseChange A f
LinearMap.liftBaseChange_comp 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type u_3} {M : Type u_4} {N : Type u_5} (A : Type u_2) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] {P : Type u_1} [AddCommMonoid P] [Module A P] [Module R P] [IsScalarTower R A P] (l : M →ₗ[R] N) (l' : N →ₗ[A] P) : l' ∘ₗ LinearMap.liftBaseChange A l = LinearMap.liftBaseChange A (↑R l' ∘ₗ l)
LinearMap.baseChange_pow 📋 Mathlib.RingTheory.TensorProduct.Basic
(R : Type u_1) (A : Type u_2) (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : Module.End R M) (n : ℕ) : LinearMap.baseChange A (f ^ n) = LinearMap.baseChange A f ^ n
LinearMap.baseChange_mul 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f g : Module.End R M) : LinearMap.baseChange A (f * g) = LinearMap.baseChange A f * LinearMap.baseChange A g
LinearMap.range_liftBaseChange 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type u_1} {M : Type u_2} {N : Type u_3} (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] (l : M →ₗ[R] N) : LinearMap.range (LinearMap.liftBaseChange A l) = Submodule.span A ↑(LinearMap.range l)
LinearMap.baseChange_smul 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (r : R) (f : M →ₗ[R] N) : LinearMap.baseChange A (r • f) = r • LinearMap.baseChange A f
LinearMap.baseChange_add 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f g : M →ₗ[R] N) : LinearMap.baseChange A (f + g) = LinearMap.baseChange A f + LinearMap.baseChange A g
LinearMap.baseChange_sub 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f g : M →ₗ[R] N) : LinearMap.baseChange A (f - g) = LinearMap.baseChange A f - LinearMap.baseChange A g
LinearMap.baseChangeHom_apply 📋 Mathlib.RingTheory.TensorProduct.Basic
(R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) : (LinearMap.baseChangeHom R A M N) f = LinearMap.baseChange A f
Algebra.TensorProduct.cancelBaseChange_tmul 📋 Mathlib.RingTheory.TensorProduct.Basic
(R : Type uR) (S : Type uS) [CommSemiring R] [CommSemiring S] [Algebra R S] (T : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring T] [CommSemiring A] [CommSemiring B] [Algebra R T] [Algebra R A] [Algebra R B] [Algebra T A] [IsScalarTower R T A] [Algebra S A] [IsScalarTower R S A] [Algebra S T] [IsScalarTower S T A] (a : A) (s : S) (b : B) : (Algebra.TensorProduct.cancelBaseChange R S T A B) (a ⊗ₜ[S] s ⊗ₜ[R] b) = (s • a) ⊗ₜ[R] b
Algebra.TensorProduct.cancelBaseChange_symm_tmul 📋 Mathlib.RingTheory.TensorProduct.Basic
(R : Type uR) (S : Type uS) [CommSemiring R] [CommSemiring S] [Algebra R S] (T : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring T] [CommSemiring A] [CommSemiring B] [Algebra R T] [Algebra R A] [Algebra R B] [Algebra T A] [IsScalarTower R T A] [Algebra S A] [IsScalarTower R S A] [Algebra S T] [IsScalarTower S T A] (a : A) (b : B) : (Algebra.TensorProduct.cancelBaseChange R S T A B).symm (a ⊗ₜ[R] b) = a ⊗ₜ[S] 1 ⊗ₜ[R] b
LinearMap.liftBaseChangeEquiv_symm_apply 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type u_4} {M : Type u_2} {N : Type u_3} (A : Type u_1) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] (l : TensorProduct R A M →ₗ[A] N) (x : M) : ((LinearMap.liftBaseChangeEquiv A).symm l) x = l (1 ⊗ₜ[R] x)
Algebra.baseChange_lmul 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {A : Type u_3} [CommSemiring A] [Algebra R A] (f : B) : LinearMap.baseChange A ((Algebra.lmul R B) f) = (Algebra.lmul A (TensorProduct R A B)) (1 ⊗ₜ[R] f)
Module.End.baseChangeHom_apply_apply 📋 Mathlib.RingTheory.TensorProduct.Basic
(R : Type u_1) (A : Type u_2) (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (a : Module.End R M) (a✝ : TensorProduct R A M) : ((Module.End.baseChangeHom R A M) a) a✝ = (TensorProduct.liftAux (↑R { toFun := fun h => h ∘ₗ a, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ ↑R (TensorProduct.AlgebraTensorModule.mk R A A M))) a✝
Module.finrank_baseChange 📋 Mathlib.LinearAlgebra.Dimension.Constructions
{R : Type u} {S : Type u'} {M' : Type v'} [Semiring R] [CommSemiring S] [AddCommMonoid M'] [StrongRankCondition R] [StrongRankCondition S] [Module S M'] [Module.Free S M'] [Algebra S R] : Module.finrank R (TensorProduct S R M') = Module.finrank S M'
Module.rank_baseChange 📋 Mathlib.LinearAlgebra.Dimension.Constructions
{R : Type u} {S : Type u'} {M' : Type v'} [Semiring R] [CommSemiring S] [AddCommMonoid M'] [StrongRankCondition R] [StrongRankCondition S] [Module S M'] [Module.Free S M'] [Algebra S R] : Module.rank R (TensorProduct S R M') = Cardinal.lift.{u, v'} (Module.rank S M')
IsBaseChange.ofEquiv 📋 Mathlib.RingTheory.IsTensorProduct
{R : Type u_1} {M : Type v₁} {N : Type v₂} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [Module R M] [Module R N] (e : M ≃ₗ[R] N) : IsBaseChange R ↑e
IsBaseChange 📋 Mathlib.RingTheory.IsTensorProduct
{R : Type u_1} {M : Type v₁} {N : Type v₂} (S : Type v₃) [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[R] N) : Prop
IsBaseChange.inductionOn 📋 Mathlib.RingTheory.IsTensorProduct
{R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) (x : N) (motive : N → Prop) (zero : motive 0) (tmul : ∀ (m : M), motive (f m)) (smul : ∀ (s : S) (n : N), motive n → motive (s • n)) (add : ∀ (n₁ n₂ : N), motive n₁ → motive n₂ → motive (n₁ + n₂)) : motive x
IsBaseChange.lift 📋 Mathlib.RingTheory.IsTensorProduct
{R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) {Q : Type u_3} [AddCommMonoid Q] [Module S Q] [Module R Q] [IsScalarTower R S Q] (g : M →ₗ[R] Q) : N →ₗ[S] Q
IsBaseChange.equiv 📋 Mathlib.RingTheory.IsTensorProduct
{R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) : TensorProduct R S M ≃ₗ[S] N
IsBaseChange.algHom_ext 📋 Mathlib.RingTheory.IsTensorProduct
{R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) {Q : Type u_3} [AddCommMonoid Q] [Module S Q] (g₁ g₂ : N →ₗ[S] Q) (e : ∀ (x : M), g₁ (f x) = g₂ (f x)) : g₁ = g₂
IsBaseChange.lift_eq 📋 Mathlib.RingTheory.IsTensorProduct
{R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) {Q : Type u_3} [AddCommMonoid Q] [Module S Q] [Module R Q] [IsScalarTower R S Q] (g : M →ₗ[R] Q) (x : M) : (h.lift g) (f x) = g x
IsBaseChange.lift_comp 📋 Mathlib.RingTheory.IsTensorProduct
{R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) {Q : Type u_3} [AddCommMonoid Q] [Module S Q] [Module R Q] [IsScalarTower R S Q] (g : M →ₗ[R] Q) : ↑R (h.lift g) ∘ₗ f = g
IsBaseChange.of_lift_unique 📋 Mathlib.RingTheory.IsTensorProduct
{R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[R] N) (h : ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q] [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g) : IsBaseChange S f
IsBaseChange.iff_lift_unique 📋 Mathlib.RingTheory.IsTensorProduct
{R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} : IsBaseChange S f ↔ ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q] [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
IsBaseChange.algHom_ext' 📋 Mathlib.RingTheory.IsTensorProduct
{R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) {Q : Type u_3} [AddCommMonoid Q] [Module S Q] [Module R Q] [IsScalarTower R S Q] (g₁ g₂ : N →ₗ[S] Q) (e : ↑R g₁ ∘ₗ f = ↑R g₂ ∘ₗ f) : g₁ = g₂
IsBaseChange.comp 📋 Mathlib.RingTheory.IsTensorProduct
{R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {T : Type u_4} {O : Type u_5} [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [AddCommMonoid O] [Module R O] [Module S O] [Module T O] [IsScalarTower S T O] [IsScalarTower R S O] [IsScalarTower R T O] {f : M →ₗ[R] N} (hf : IsBaseChange S f) {g : N →ₗ[S] O} (hg : IsBaseChange T g) : IsBaseChange T (↑R g ∘ₗ f)
IsBaseChange.of_comp 📋 Mathlib.RingTheory.IsTensorProduct
{R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {T : Type u_4} {O : Type u_5} [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [AddCommMonoid O] [Module R O] [Module S O] [Module T O] [IsScalarTower S T O] [IsScalarTower R S O] [IsScalarTower R T O] {f : M →ₗ[R] N} (hf : IsBaseChange S f) {h : N →ₗ[S] O} (hc : IsBaseChange T (↑R h ∘ₗ f)) : IsBaseChange T h
IsBaseChange.comp_iff 📋 Mathlib.RingTheory.IsTensorProduct
{R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {T : Type u_4} {O : Type u_5} [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [AddCommMonoid O] [Module R O] [Module S O] [Module T O] [IsScalarTower S T O] [IsScalarTower R S O] [IsScalarTower R T O] {f : M →ₗ[R] N} (hf : IsBaseChange S f) {h : N →ₗ[S] O} : IsBaseChange T (↑R h ∘ₗ f) ↔ IsBaseChange T h
isBaseChange_tensorProduct_map 📋 Mathlib.RingTheory.IsTensorProduct
{R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {P : Type u_2} [AddCommMonoid P] [Module R P] (A : Type u_4) [CommSemiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Module S M] [IsScalarTower R S M] [Module A N] [IsScalarTower S A N] [IsScalarTower R A N] {f : M →ₗ[S] N} (hf : IsBaseChange A f) : IsBaseChange A (TensorProduct.AlgebraTensorModule.map f LinearMap.id)
IsBaseChange.equiv_tmul 📋 Mathlib.RingTheory.IsTensorProduct
{R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) (s : S) (m : M) : h.equiv (s ⊗ₜ[R] m) = s • f m
IsBaseChange.of_equiv 📋 Mathlib.RingTheory.IsTensorProduct
{R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (e : TensorProduct R S M ≃ₗ[S] N) (he : ∀ (x : M), e (1 ⊗ₜ[R] x) = f x) : IsBaseChange S f
IsBaseChange.equiv_symm_apply 📋 Mathlib.RingTheory.IsTensorProduct
{R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) (m : M) : h.equiv.symm (f m) = 1 ⊗ₜ[R] m
TensorProduct.isBaseChange 📋 Mathlib.RingTheory.IsTensorProduct
(R : Type u_1) (M : Type v₁) (S : Type v₃) [AddCommMonoid M] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] : IsBaseChange S ((TensorProduct.mk R S M) 1)
Algebra.EssFiniteType.baseChange 📋 Mathlib.RingTheory.EssentialFiniteness
(R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [h : Algebra.EssFiniteType R S] : Algebra.EssFiniteType T (TensorProduct R T S)
KaehlerDifferential.mapBaseChange 📋 Mathlib.RingTheory.Kaehler.Basic
(R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] : TensorProduct A B (Ω[A⁄R]) →ₗ[B] Ω[B⁄R]
KaehlerDifferential.mapBaseChange_surjective 📋 Mathlib.RingTheory.Kaehler.Basic
(R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (h : Function.Surjective ⇑(algebraMap A B)) : Function.Surjective ⇑(KaehlerDifferential.mapBaseChange R A B)
KaehlerDifferential.exact_mapBaseChange_map 📋 Mathlib.RingTheory.Kaehler.Basic
(R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] : Function.Exact ⇑(KaehlerDifferential.mapBaseChange R A B) ⇑(KaehlerDifferential.map R A B B)
KaehlerDifferential.mapBaseChange_tmul 📋 Mathlib.RingTheory.Kaehler.Basic
(R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (x : B) (y : Ω[A⁄R]) : (KaehlerDifferential.mapBaseChange R A B) (x ⊗ₜ[A] y) = x • (KaehlerDifferential.map R R A B) y
KaehlerDifferential.range_mapBaseChange 📋 Mathlib.RingTheory.Kaehler.Basic
(R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] : LinearMap.range (KaehlerDifferential.mapBaseChange R A B) = LinearMap.ker (KaehlerDifferential.map R A B B)
KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange 📋 Mathlib.RingTheory.Kaehler.Basic
(R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (h : Function.Surjective ⇑(algebraMap A B)) : Function.Exact ⇑(KaehlerDifferential.kerCotangentToTensor R A B) ⇑(KaehlerDifferential.mapBaseChange R A B)
IsLocalizedModule.isBaseChange 📋 Mathlib.RingTheory.Localization.BaseChange
{R : Type u_1} [CommSemiring R] (S : Submonoid R) (A : Type u_2) [CommSemiring A] [Algebra R A] [IsLocalization S A] {M : Type u_3} [AddCommMonoid M] [Module R M] {M' : Type u_4} [AddCommMonoid M'] [Module R M'] [Module A M'] [IsScalarTower R A M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] : IsBaseChange A f
isLocalizedModule_iff_isBaseChange 📋 Mathlib.RingTheory.Localization.BaseChange
{R : Type u_1} [CommSemiring R] (S : Submonoid R) (A : Type u_2) [CommSemiring A] [Algebra R A] [IsLocalization S A] {M : Type u_3} [AddCommMonoid M] [Module R M] {M' : Type u_4} [AddCommMonoid M'] [Module R M'] [Module A M'] [IsScalarTower R A M'] (f : M →ₗ[R] M') : IsLocalizedModule S f ↔ IsBaseChange A f
Module.Flat.isBaseChange 📋 Mathlib.RingTheory.Flat.Stability
(R : Type u) (S : Type v) (M : Type w) [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module.Flat R M] (N : Type t) [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) : Module.Flat S N
Module.Flat.baseChange 📋 Mathlib.RingTheory.Flat.Stability
(R : Type u) (S : Type v) (M : Type w) [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module.Flat R M] : Module.Flat S (TensorProduct R S M)
RingHom.IsStableUnderBaseChange 📋 Mathlib.RingTheory.RingHomProperties
(P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : Prop
RingHom.IsStableUnderBaseChange.and 📋 Mathlib.RingTheory.RingHomProperties
{P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => P) (hQ : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q) : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] f => P f ∧ Q f
RingHom.IsStableUnderBaseChange.mk 📋 Mathlib.RingTheory.RingHomProperties
{P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (h₁ : RingHom.RespectsIso P) (h₂ : ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom) : RingHom.IsStableUnderBaseChange P
RingHom.IsStableUnderBaseChange.pushout_inl 📋 Mathlib.RingTheory.RingHomProperties
{P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.IsStableUnderBaseChange P) (hP' : RingHom.RespectsIso P) {R S T : CommRingCat} (f : R ⟶ S) (g : R ⟶ T) (H : P (CommRingCat.Hom.hom g)) : P (CommRingCat.Hom.hom (CategoryTheory.Limits.pushout.inl f g))
RingHom.IsStableUnderBaseChange.localizationPreserves 📋 Mathlib.RingTheory.LocalProperties.Basic
{P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.IsStableUnderBaseChange P) : RingHom.LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => P
RingHom.IsStableUnderBaseChange.of_isLocalization 📋 Mathlib.RingTheory.LocalProperties.Basic
{P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.IsStableUnderBaseChange P) {R S Rᵣ Sᵣ : Type u} [CommRing R] [CommRing S] [CommRing Rᵣ] [CommRing Sᵣ] [Algebra R Rᵣ] [Algebra S Sᵣ] [Algebra R S] [Algebra R Sᵣ] [Algebra Rᵣ Sᵣ] [IsScalarTower R S Sᵣ] [IsScalarTower R Rᵣ Sᵣ] (M : Submonoid R) [IsLocalization M Rᵣ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sᵣ] (h : P (algebraMap R S)) : P (algebraMap Rᵣ Sᵣ)
RingHom.IsStableUnderBaseChange.isLocalization_map 📋 Mathlib.RingTheory.LocalProperties.Basic
{P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.IsStableUnderBaseChange P) {R S Rᵣ Sᵣ : Type u} [CommRing R] [CommRing S] [CommRing Rᵣ] [CommRing Sᵣ] [Algebra R Rᵣ] [Algebra S Sᵣ] (M : Submonoid R) [IsLocalization M Rᵣ] (f : R →+* S) [IsLocalization (Submonoid.map f M) Sᵣ] (hf : P f) : P (IsLocalization.map Sᵣ f ⋯)
RingHom.Flat.isStableUnderBaseChange 📋 Mathlib.RingTheory.RingHom.Flat
: RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => RingHom.Flat
Basis.baseChange_end 📋 Mathlib.RingTheory.TensorProduct.Free
{R : Type u_1} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (A : Type u_5) [CommSemiring A] [Algebra R A] [DecidableEq ι] (b : Basis ι R M) (ij : ι × ι) : LinearMap.baseChange A (b.end ij) = (Algebra.TensorProduct.basis A b).end ij
Basis.baseChange_linearMap 📋 Mathlib.RingTheory.TensorProduct.Free
{R : Type u_1} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] {ι' : Type u_3} {N : Type u_4} [Fintype ι'] [DecidableEq ι'] [AddCommMonoid N] [Module R N] (A : Type u_5) [CommSemiring A] [Algebra R A] (b : Basis ι R M) (b' : Basis ι' R N) (ij : ι × ι') : LinearMap.baseChange A ((b'.linearMap b) ij) = ((Algebra.TensorProduct.basis A b').linearMap (Algebra.TensorProduct.basis A b)) ij
LinearMap.toMatrix_baseChange 📋 Mathlib.RingTheory.TensorProduct.Free
{R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι : Type u_4} {ι₂ : Type u_5} (A : Type u_6) [Fintype ι] [Finite ι₂] [DecidableEq ι] [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) (b₁ : Basis ι R M₁) (b₂ : Basis ι₂ R M₂) : (LinearMap.toMatrix (Algebra.TensorProduct.basis A b₁) (Algebra.TensorProduct.basis A b₂)) (LinearMap.baseChange A f) = ((LinearMap.toMatrix b₁ b₂) f).map ⇑(algebraMap R A)
LinearMap.trace_baseChange 📋 Mathlib.LinearAlgebra.Trace
{R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) (A : Type u_6) [CommRing A] [Algebra R A] : (LinearMap.trace A (TensorProduct R A M)) (LinearMap.baseChange A f) = (algebraMap R A) ((LinearMap.trace R M) f)
CategoryTheory.MorphismProperty.IsStableUnderBaseChange 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) : Prop
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) : Prop
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.isomorphisms 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
(C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.MorphismProperty.isomorphisms C).IsStableUnderBaseChange
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.monomorphisms 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
(C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.MorphismProperty.monomorphisms C).IsStableUnderBaseChange
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.epimorphisms 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
(C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.MorphismProperty.epimorphisms C).IsStableUnderCobaseChange
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.isomorphisms 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] : (CategoryTheory.MorphismProperty.isomorphisms C).IsStableUnderCobaseChange
CategoryTheory.MorphismProperty.instIsStableUnderBaseChangePullbacks 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) : P.pullbacks.IsStableUnderBaseChange
CategoryTheory.MorphismProperty.instIsStableUnderCobaseChangePushouts 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) : P.pushouts.IsStableUnderCobaseChange
CategoryTheory.MorphismProperty.universally_isStableUnderBaseChange 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) : P.universally.IsStableUnderBaseChange
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.respectsIso 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] : P.RespectsIso
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.respectsIso 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderCobaseChange] : P.RespectsIso
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.hasOfPostcompProperty_monomorphisms 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] : P.HasOfPostcompProperty (CategoryTheory.MorphismProperty.monomorphisms C)
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.hasOfPrecompProperty_epimorphisms 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderCobaseChange] : P.HasOfPrecompProperty (CategoryTheory.MorphismProperty.epimorphisms C)
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.universally_eq 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [hP : P.IsStableUnderBaseChange] : P.universally = P
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.op 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] : P.op.IsStableUnderCobaseChange
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.op 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderCobaseChange] : P.op.IsStableUnderBaseChange
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.unop 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty Cᵒᵖ} [P.IsStableUnderBaseChange] : P.unop.IsStableUnderCobaseChange
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.unop 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty Cᵒᵖ} [P.IsStableUnderCobaseChange] : P.unop.IsStableUnderBaseChange
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.diagonal 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] [P.RespectsIso] : P.diagonal.IsStableUnderBaseChange
CategoryTheory.MorphismProperty.isStableUnderBaseChange_iff_pullbacks_le 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) : P.IsStableUnderBaseChange ↔ P.pullbacks ≤ P
CategoryTheory.MorphismProperty.isStableUnderCobaseChange_iff_pushouts_le 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} : P.IsStableUnderCobaseChange ↔ P.pushouts ≤ P
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inf 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] : (P ⊓ Q).IsStableUnderBaseChange
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.inf 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.MorphismProperty C} [P.IsStableUnderCobaseChange] [Q.IsStableUnderCobaseChange] : (P ⊓ Q).IsStableUnderCobaseChange
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.fst 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [CategoryTheory.Limits.HasPullback f g] (H : P g) : P (CategoryTheory.Limits.pullback.fst f g)
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inl 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderCobaseChange] {A B A' : C} (f : A ⟶ A') (g : A ⟶ B) [CategoryTheory.Limits.HasPushout f g] (H : P g) : P (CategoryTheory.Limits.pushout.inl f g)
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inr 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderCobaseChange] {A B A' : C} (f : A ⟶ A') (g : A ⟶ B) [CategoryTheory.Limits.HasPushout f g] (H : P f) : P (CategoryTheory.Limits.pushout.inr f g)
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.snd 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [CategoryTheory.Limits.HasPullback f g] (H : P f) : P (CategoryTheory.Limits.pullback.snd f g)
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.mk' 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.RespectsIso] (hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : CategoryTheory.Limits.HasPullback f g], P g → P (CategoryTheory.Limits.pullback.fst f g)) : P.IsStableUnderBaseChange
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.mk' 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.RespectsIso] (hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst : CategoryTheory.Limits.HasPushout f g], P f → P (CategoryTheory.Limits.pushout.inr f g)) : P.IsStableUnderCobaseChange
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.mk 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (of_isPullback : ∀ {X Y Y' S : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X}, CategoryTheory.IsPullback f' g' g f → P g → P g') : P.IsStableUnderBaseChange
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.of_isPullback 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C} [self : P.IsStableUnderBaseChange] {X Y Y' S : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X} (sq : CategoryTheory.IsPullback f' g' g f) (hg : P g) : P g'
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.mk 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (of_isPushout : ∀ {A A' B B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'}, CategoryTheory.IsPushout g f f' g' → P f → P f') : P.IsStableUnderCobaseChange
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.of_isPushout 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C} [self : P.IsStableUnderCobaseChange] {A A' B B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : CategoryTheory.IsPushout g f f' g') (hf : P f) : P f'
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.pullback_map 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [CategoryTheory.Limits.HasPullbacks C] [P.IsStableUnderBaseChange] [P.IsStableUnderComposition] {S X X' Y Y' : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : X' ⟶ S} {g' : Y' ⟶ S} {i₁ : X ⟶ X'} {i₂ : Y ⟶ Y'} (h₁ : P i₁) (h₂ : P i₂) (e₁ : f = CategoryTheory.CategoryStruct.comp i₁ f') (e₂ : g = CategoryTheory.CategoryStruct.comp i₂ g') : P (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
CategoryTheory.MorphismProperty.baseChange_obj 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [CategoryTheory.Limits.HasPullbacks C] [P.IsStableUnderBaseChange] {S S' : C} (f : S' ⟶ S) (X : CategoryTheory.Over S) (H : P X.hom) : P ((CategoryTheory.Over.pullback f).obj X).hom
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.baseChange_obj 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [CategoryTheory.Limits.HasPullbacks C] [P.IsStableUnderBaseChange] {S S' : C} (f : S' ⟶ S) (X : CategoryTheory.Over S) (H : P X.hom) : P ((CategoryTheory.Over.pullback f).obj X).hom
CategoryTheory.MorphismProperty.baseChange_map 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [CategoryTheory.Limits.HasPullbacks C] [P.IsStableUnderBaseChange] {S S' : C} (f : S' ⟶ S) {X Y : CategoryTheory.Over S} (g : X ⟶ Y) (H : P g.left) : P ((CategoryTheory.Over.pullback f).map g).left
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.baseChange_map 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [CategoryTheory.Limits.HasPullbacks C] [P.IsStableUnderBaseChange] {S S' : C} (f : S' ⟶ S) {X Y : CategoryTheory.Over S} (g : X ⟶ Y) (H : P g.left) : P ((CategoryTheory.Over.pullback f).map g).left
LieSubmodule.baseChange 📋 Mathlib.Algebra.Lie.BaseChange
{R : Type u_1} (A : Type u_2) {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [Algebra R A] (N : LieSubmodule R L M) : LieSubmodule A (TensorProduct R A L) (TensorProduct R A M)
LieSubmodule.baseChange.eq_1 📋 Mathlib.Algebra.Lie.BaseChange
{R : Type u_1} (A : Type u_2) {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [Algebra R A] (N : LieSubmodule R L M) : LieSubmodule.baseChange A N = { toSubmodule := Submodule.baseChange A ↑N, lie_mem := ⋯ }
LieSubmodule.coe_baseChange 📋 Mathlib.Algebra.Lie.BaseChange
(R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [Algebra R A] (N : LieSubmodule R L M) : ↑(LieSubmodule.baseChange A N) = Submodule.baseChange A ↑N
LieSubmodule.baseChange_bot 📋 Mathlib.Algebra.Lie.BaseChange
(R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [Algebra R A] : LieSubmodule.baseChange A ⊥ = ⊥
LieSubmodule.baseChange_top 📋 Mathlib.Algebra.Lie.BaseChange
(R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [Algebra R A] : LieSubmodule.baseChange A ⊤ = ⊤
LieSubmodule.tmul_mem_baseChange_of_mem 📋 Mathlib.Algebra.Lie.BaseChange
{R : Type u_1} {A : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [Algebra R A] {N : LieSubmodule R L M} (a : A) {m : M} (hm : m ∈ N) : a ⊗ₜ[R] m ∈ LieSubmodule.baseChange A N
LieSubmodule.lie_baseChange 📋 Mathlib.Algebra.Lie.BaseChange
(R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [Algebra R A] {I : LieIdeal R L} {N : LieSubmodule R L M} : LieSubmodule.baseChange A ⁅I, N⁆ = ⁅LieSubmodule.baseChange A I, LieSubmodule.baseChange A N⁆
LieSubmodule.mem_baseChange_iff 📋 Mathlib.Algebra.Lie.BaseChange
(R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [Algebra R A] {N : LieSubmodule R L M} {m : TensorProduct R A M} : m ∈ LieSubmodule.baseChange A N ↔ m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
LieModule.toEnd_baseChange 📋 Mathlib.Algebra.Lie.BaseChange
(R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [Algebra R A] (x : L) : (LieModule.toEnd A (TensorProduct R A L) (TensorProduct R A M)) (1 ⊗ₜ[R] x) = LinearMap.baseChange A ((LieModule.toEnd R L M) x)
LieAlgebra.derivedSeries_baseChange 📋 Mathlib.Algebra.Lie.Solvable
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type u_1} [CommRing A] [Algebra R A] (k : ℕ) : LieAlgebra.derivedSeries A (TensorProduct R A L) k = LieSubmodule.baseChange A (LieAlgebra.derivedSeries R L k)
LieAlgebra.derivedSeriesOfIdeal_baseChange 📋 Mathlib.Algebra.Lie.Solvable
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) {A : Type u_1} [CommRing A] [Algebra R A] (k : ℕ) : LieAlgebra.derivedSeriesOfIdeal A (TensorProduct R A L) k (LieSubmodule.baseChange A I) = LieSubmodule.baseChange A (LieAlgebra.derivedSeriesOfIdeal R L k I)
LieSubmodule.lowerCentralSeries_tensor_eq_baseChange 📋 Mathlib.Algebra.Lie.Nilpotent
(R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [Algebra R A] (k : ℕ) : LieModule.lowerCentralSeries A (TensorProduct R A L) (TensorProduct R A M) k = LieSubmodule.baseChange A (LieModule.lowerCentralSeries R L M k)
LinearMap.toMvPolynomial_baseChange 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
{R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Finite ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (i : ι₂) (A : Type u_6) [CommRing A] [Algebra R A] : LinearMap.toMvPolynomial (Algebra.TensorProduct.basis A b₁) (Algebra.TensorProduct.basis A b₂) (LinearMap.baseChange A f) i = (MvPolynomial.map (algebraMap R A)) (LinearMap.toMvPolynomial b₁ b₂ f i)
LinearMap.polyCharpolyAux_baseChange 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
{R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Basis ι R L) (bₘ : Basis ιM R M) (A : Type u_8) [CommRing A] [Algebra R A] : (LinearMap.tensorProduct R A M M ∘ₗ LinearMap.baseChange A φ).polyCharpolyAux (Algebra.TensorProduct.basis A b) (Algebra.TensorProduct.basis A bₘ) = Polynomial.map (MvPolynomial.map (algebraMap R A)) (φ.polyCharpolyAux b bₘ)
LinearMap.polyCharpoly_baseChange 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
{R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (b : Basis ι R L) (A : Type u_8) [CommRing A] [Algebra R A] : (LinearMap.tensorProduct R A M M ∘ₗ LinearMap.baseChange A φ).polyCharpoly (Algebra.TensorProduct.basis A b) = Polynomial.map (MvPolynomial.map (algebraMap R A)) (φ.polyCharpoly b)
IsBaseChange.finrank_eq 📋 Mathlib.LinearAlgebra.Dimension.Localization
{R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {T : Type uT} [CommRing T] [NoZeroDivisors T] [Algebra R T] [FaithfulSMul R T] {P : Type uP} [AddCommGroup P] [Module R P] [Module T P] [IsScalarTower R T P] {g : M →ₗ[R] P} (bc : IsBaseChange T g) : Module.finrank T P = Module.finrank R M
IsBaseChange.rank_eq 📋 Mathlib.LinearAlgebra.Dimension.Localization
{R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {T : Type uT} [CommRing T] [NoZeroDivisors T] [Algebra R T] [FaithfulSMul R T] {P : Type uM} [AddCommGroup P] [Module R P] [Module T P] [IsScalarTower R T P] {g : M →ₗ[R] P} (bc : IsBaseChange T g) : Module.rank T P = Module.rank R M
IsBaseChange.lift_rank_eq 📋 Mathlib.LinearAlgebra.Dimension.Localization
{R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {T : Type uT} [CommRing T] [NoZeroDivisors T] [Algebra R T] [FaithfulSMul R T] {P : Type uP} [AddCommGroup P] [Module R P] [Module T P] [IsScalarTower R T P] {g : M →ₗ[R] P} (bc : IsBaseChange T g) : Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
IsBaseChange.finrank_eq_of_le_nonZeroDivisors 📋 Mathlib.LinearAlgebra.Dimension.Localization
{R : Type uR} (S : Type uS) {M : Type uM} {N : Type uN} [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] {p : Submonoid R} [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] (hp : p ≤ nonZeroDivisors R) [Module.Free S N] [StrongRankCondition S] {T : Type uT} [CommRing T] [Algebra R T] (hpT : Algebra.algebraMapSubmonoid T p ≤ nonZeroDivisors T) [StrongRankCondition (TensorProduct R S T)] {P : Type uP} [AddCommGroup P] [Module R P] [Module T P] [IsScalarTower R T P] {g : M →ₗ[R] P} (bc : IsBaseChange T g) : Module.finrank T P = Module.finrank R M
IsBaseChange.rank_eq_of_le_nonZeroDivisors 📋 Mathlib.LinearAlgebra.Dimension.Localization
{R : Type uR} (S : Type uS) {M : Type uM} {N : Type uN} [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] {p : Submonoid R} [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] (hp : p ≤ nonZeroDivisors R) [Module.Free S N] [StrongRankCondition S] {T : Type uT} [CommRing T] [Algebra R T] (hpT : Algebra.algebraMapSubmonoid T p ≤ nonZeroDivisors T) [StrongRankCondition (TensorProduct R S T)] {P : Type uM} [AddCommGroup P] [Module R P] [Module T P] [IsScalarTower R T P] {g : M →ₗ[R] P} (bc : IsBaseChange T g) : Module.rank T P = Module.rank R M
IsBaseChange.lift_rank_eq_of_le_nonZeroDivisors 📋 Mathlib.LinearAlgebra.Dimension.Localization
{R : Type uR} (S : Type uS) {M : Type uM} {N : Type uN} [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N] {p : Submonoid R} [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] (hp : p ≤ nonZeroDivisors R) [Module.Free S N] [StrongRankCondition S] {T : Type uT} [CommRing T] [Algebra R T] (hpT : Algebra.algebraMapSubmonoid T p ≤ nonZeroDivisors T) [StrongRankCondition (TensorProduct R S T)] {P : Type uP} [AddCommGroup P] [Module R P] [Module T P] [IsScalarTower R T P] {g : M →ₗ[R] P} (bc : IsBaseChange T g) : Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
Subbimodule.baseChange 📋 Mathlib.Algebra.Module.Bimodule
{R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Semiring B] [Module A M] [Module B M] [Algebra R A] [Algebra R B] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] (S : Type u_5) [CommSemiring S] [Module S M] [Algebra S A] [Algebra S B] [IsScalarTower S A M] [IsScalarTower S B M] (p : Submodule (TensorProduct R A B) M) : Submodule (TensorProduct S A B) M
Subbimodule.coe_baseChange 📋 Mathlib.Algebra.Module.Bimodule
{R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Semiring B] [Module A M] [Module B M] [Algebra R A] [Algebra R B] [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] (S : Type u_5) [CommSemiring S] [Module S M] [Algebra S A] [Algebra S B] [IsScalarTower S A M] [IsScalarTower S B M] (p : Submodule (TensorProduct R A B) M) : ↑(Subbimodule.baseChange S p) = ↑p
FinitePresentation.of_isBaseChange 📋 Mathlib.Algebra.Module.FinitePresentation
{R : Type u_2} {M : Type u_4} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {A : Type u_1} [CommRing A] [Algebra R A] [Module A N] [IsScalarTower R A N] (f : M →ₗ[R] N) (h : IsBaseChange A f) [Module.FinitePresentation R M] : Module.FinitePresentation A N
Algebra.Extension.baseChange 📋 Mathlib.RingTheory.Extension
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] (P : Algebra.Extension R S) : Algebra.Extension T (TensorProduct R T S)
Algebra.Generators.baseChange 📋 Mathlib.RingTheory.Generators
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] (P : Algebra.Generators R S) : Algebra.Generators T (TensorProduct R T S)
Algebra.Generators.baseChange_vars 📋 Mathlib.RingTheory.Generators
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] (P : Algebra.Generators R S) : P.baseChange.vars = P.vars
Algebra.Generators.baseChange_val 📋 Mathlib.RingTheory.Generators
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] (P : Algebra.Generators R S) (x : P.vars) : P.baseChange.val x = 1 ⊗ₜ[R] P.val x
Algebra.Presentation.baseChange 📋 Mathlib.RingTheory.Presentation
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_1) [CommRing T] [Algebra R T] (P : Algebra.Presentation R S) : Algebra.Presentation T (TensorProduct R T S)
Algebra.Presentation.baseChange_isFinite 📋 Mathlib.RingTheory.Presentation
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_3) [CommRing T] [Algebra R T] (P : Algebra.Presentation R S) [P.IsFinite] : (Algebra.Presentation.baseChange T P).IsFinite
Algebra.Presentation.baseChange_rels 📋 Mathlib.RingTheory.Presentation
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_1) [CommRing T] [Algebra R T] (P : Algebra.Presentation R S) : (Algebra.Presentation.baseChange T P).rels = P.rels
Algebra.Presentation.baseChange_toGenerators 📋 Mathlib.RingTheory.Presentation
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_1) [CommRing T] [Algebra R T] (P : Algebra.Presentation R S) : (Algebra.Presentation.baseChange T P).toGenerators = P.baseChange
Algebra.Presentation.baseChange_relation 📋 Mathlib.RingTheory.Presentation
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_1) [CommRing T] [Algebra R T] (P : Algebra.Presentation R S) (i : P.rels) : (Algebra.Presentation.baseChange T P).relation i = (MvPolynomial.map (algebraMap R T)) (P.relation i)
AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange 📋 Mathlib.AlgebraicGeometry.OpenImmersion
: AlgebraicGeometry.IsOpenImmersion.IsStableUnderBaseChange
RingHom.surjective_isStableUnderBaseChange 📋 Mathlib.RingTheory.RingHom.Surjective
: RingHom.IsStableUnderBaseChange fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f
AlgebraicGeometry.AffineTargetMorphismProperty.IsStableUnderBaseChange 📋 Mathlib.AlgebraicGeometry.Morphisms.Basic
(P : AlgebraicGeometry.AffineTargetMorphismProperty) : Prop
AlgebraicGeometry.instHasOfPostcompPropertySchemeIsOpenImmersionOfIsStableUnderBaseChange 📋 Mathlib.AlgebraicGeometry.Morphisms.Basic
(P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] : P.HasOfPostcompProperty AlgebraicGeometry.IsOpenImmersion
AlgebraicGeometry.HasAffineProperty.isStableUnderBaseChange 📋 Mathlib.AlgebraicGeometry.Morphisms.Basic
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty} [AlgebraicGeometry.HasAffineProperty P Q] (hP' : Q.IsStableUnderBaseChange) : P.IsStableUnderBaseChange
AlgebraicGeometry.AffineTargetMorphismProperty.IsStableUnderBaseChange.mk 📋 Mathlib.AlgebraicGeometry.Morphisms.Basic
(P : AlgebraicGeometry.AffineTargetMorphismProperty) [P.toProperty.RespectsIso] (H : ∀ ⦃X Y S : AlgebraicGeometry.Scheme⦄ [inst : AlgebraicGeometry.IsAffine S] [inst_1 : AlgebraicGeometry.IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (CategoryTheory.Limits.pullback.fst f g)) : P.IsStableUnderBaseChange
AlgebraicGeometry.AffineTargetMorphismProperty.isStableUnderBaseChange_of_isStableUnderBaseChangeOnAffine_of_isLocalAtTarget 📋 Mathlib.AlgebraicGeometry.Morphisms.Constructors
(P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocalAtTarget P] (hP₂ : (AlgebraicGeometry.AffineTargetMorphismProperty.of P).IsStableUnderBaseChange) : P.IsStableUnderBaseChange
AlgebraicGeometry.quasiCompact_isStableUnderBaseChange 📋 Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
: CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.QuasiCompact
AlgebraicGeometry.quasiSeparated_isStableUnderBaseChange 📋 Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
: CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.QuasiSeparated
AlgebraicGeometry.isAffineHom_isStableUnderBaseChange 📋 Mathlib.AlgebraicGeometry.Morphisms.Affine
: CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.IsAffineHom
RingHom.locally_isStableUnderBaseChange 📋 Mathlib.RingTheory.RingHom.Locally
{P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) (hPb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => P) : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => RingHom.Locally fun {R S} [CommRing R] [CommRing S] => P
AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange 📋 Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] (hP : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q) : P.IsStableUnderBaseChange
RingHom.IsStableUnderBaseChange.pullback_fst_appTop 📋 Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
(P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) (hP : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => P) (hP' : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) {X Y S : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] [AlgebraicGeometry.IsAffine S] (f : X ⟶ S) (g : Y ⟶ S) (H : P (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop g))) : P (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop (CategoryTheory.Limits.pullback.fst f g)))
RingHom.IsStableUnderBaseChange.pullback_fst_app_top 📋 Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
(P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) (hP : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => P) (hP' : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) {X Y S : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] [AlgebraicGeometry.IsAffine S] (f : X ⟶ S) (g : Y ⟶ S) (H : P (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop g))) : P (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop (CategoryTheory.Limits.pullback.fst f g)))
AlgebraicGeometry.affineAnd_isStableUnderBaseChange 📋 Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
{Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) (hQb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q) : (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q).IsStableUnderBaseChange
AlgebraicGeometry.HasAffineProperty.affineAnd_isStableUnderBaseChange 📋 Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
{Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} : AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q) → ∀ (hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) (hQb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q), P.IsStableUnderBaseChange
RingHom.SurjectiveOnStalks.baseChange 📋 Mathlib.RingTheory.SurjectiveOnStalks
{R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {T : Type u_3} [CommRing T] [Algebra R T] [Algebra R S] (hf : (algebraMap R T).SurjectiveOnStalks) : (algebraMap S (TensorProduct R S T)).SurjectiveOnStalks
AlgebraicGeometry.SurjectiveOnStalks.stableUnderBaseChange 📋 Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
: CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.SurjectiveOnStalks
AlgebraicGeometry.IsPreimmersion.instIsStableUnderBaseChangeScheme 📋 Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
: CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.IsPreimmersion
Algebra.FinitePresentation.baseChange 📋 Mathlib.RingTheory.FiniteStability
{R : Type w₁} [CommRing R] {A : Type w₂} [CommRing A] [Algebra R A] (B : Type w₃) [CommRing B] [Algebra R B] [Algebra.FinitePresentation R A] : Algebra.FinitePresentation B (TensorProduct R B A)
Algebra.FiniteType.baseChange 📋 Mathlib.RingTheory.FiniteStability
{R : Type w₁} [CommRing R] {A : Type w₂} [CommRing A] [Algebra R A] (B : Type w₃) [CommRing B] [Algebra R B] [hfa : Algebra.FiniteType R A] : Algebra.FiniteType B (TensorProduct R B A)
Algebra.FiniteType.baseChangeAux_surj 📋 Mathlib.RingTheory.FiniteStability
{R : Type w₁} [CommRing R] {A : Type w₂} [CommRing A] [Algebra R A] (B : Type w₃) [CommRing B] [Algebra R B] {σ : Type u_1} {f : MvPolynomial σ R →ₐ[R] A} (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(Algebra.TensorProduct.map (AlgHom.id B B) f)
RingHom.finite_isStableUnderBaseChange 📋 Mathlib.RingTheory.RingHom.Finite
: RingHom.IsStableUnderBaseChange @RingHom.Finite
RingHom.finiteType_isStableUnderBaseChange 📋 Mathlib.RingTheory.RingHom.FiniteType
: RingHom.IsStableUnderBaseChange @RingHom.FiniteType
AlgebraicGeometry.locallyOfFiniteType_isStableUnderBaseChange 📋 Mathlib.AlgebraicGeometry.Morphisms.FiniteType
: CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.LocallyOfFiniteType
AlgebraicGeometry.IsClosedImmersion.isStableUnderBaseChange 📋 Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
: CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.IsClosedImmersion
AlgebraicGeometry.Surjective.instIsStableUnderBaseChangeScheme 📋 Mathlib.AlgebraicGeometry.PullbackCarrier
: CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.Surjective
AlgebraicGeometry.universallyClosed_isStableUnderBaseChange 📋 Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
: CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.UniversallyClosed
RingHom.isIntegral_isStableUnderBaseChange 📋 Mathlib.RingTheory.RingHom.Integral
: RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral
AlgebraicGeometry.IsIntegralHom.instIsStableUnderBaseChangeScheme 📋 Mathlib.AlgebraicGeometry.Morphisms.Integral
: CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.IsIntegralHom
AlgebraicGeometry.IsFinite.instIsStableUnderBaseChangeScheme 📋 Mathlib.AlgebraicGeometry.Morphisms.Finite
: CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.IsFinite
RingHom.finitePresentation_isStableUnderBaseChange 📋 Mathlib.RingTheory.RingHom.FinitePresentation
: RingHom.IsStableUnderBaseChange @RingHom.FinitePresentation
LinearMap.charpoly_baseChange 📋 Mathlib.LinearAlgebra.Charpoly.BaseChange
{R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) (A : Type u_3) [CommRing A] [Algebra R A] : (LinearMap.baseChange A f).charpoly = Polynomial.map (algebraMap R A) f.charpoly
LinearMap.det_baseChange 📋 Mathlib.LinearAlgebra.Charpoly.BaseChange
{R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] {A : Type u_3} [CommRing A] [Algebra R A] (f : M →ₗ[R] M) : LinearMap.det (LinearMap.baseChange A f) = (algebraMap R A) (LinearMap.det f)
AlgebraicGeometry.locallyOfFinitePresentation_isStableUnderBaseChange 📋 Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
: CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.LocallyOfFinitePresentation
WeierstrassCurve.baseChange 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRing A] [Algebra R A] : WeierstrassCurve A
WeierstrassCurve.map_baseChange 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) {S : Type s} [CommRing S] [Algebra R S] {A : Type v} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type w} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (g : A →ₐ[S] B) : (W.baseChange A).map ↑g = W.baseChange B
WeierstrassCurve.VariableChange.baseChange 📋 Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
{R : Type u} [CommRing R] (A : Type v) [CommRing A] (C : WeierstrassCurve.VariableChange R) [Algebra R A] : WeierstrassCurve.VariableChange A
WeierstrassCurve.VariableChange.map_baseChange 📋 Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
{R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) {S : Type s} [CommRing S] [Algebra R S] {A : Type v} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type w} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (ψ : A →ₐ[S] B) : WeierstrassCurve.VariableChange.map (↑ψ) (WeierstrassCurve.VariableChange.baseChange A C) = WeierstrassCurve.VariableChange.baseChange B C
WeierstrassCurve.Affine.Equation.baseChange 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
{R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W : WeierstrassCurve.Affine R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) {x y : A} (h : (WeierstrassCurve.baseChange W A).toAffine.Equation x y) : (WeierstrassCurve.baseChange W B).toAffine.Equation (f x) (f y)
WeierstrassCurve.Affine.baseChange_equation 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
{R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W : WeierstrassCurve.Affine R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B] [IsScalarTower R S B] {f : A →ₐ[S] B} (x y : A) (hf : Function.Injective ⇑f) : (WeierstrassCurve.baseChange W B).toAffine.Equation (f x) (f y) ↔ (WeierstrassCurve.baseChange W A).toAffine.Equation x y

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 19971e9 serving mathlib revision bce1d65