Loogle!
Result
Found 152 declarations mentioning TensorProduct and Prod.
- TensorProduct.SMul.aux 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
{R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R' : Type u_11} [SMul R' M] (r : R') : FreeAddMonoid (M × N) →+ TensorProduct R M N - TensorProduct.SMul.aux_of 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
{R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R' : Type u_11} [SMul R' M] (r : R') (m : M) (n : N) : (TensorProduct.SMul.aux r) (FreeAddMonoid.of (m, n)) = (r • m) ⊗ₜ[R] n - Module.End.baseChangeHom_apply_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
(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✝ - TensorProduct.directSum 📋 Mathlib.LinearAlgebra.DirectSum.TensorProduct
(R : Type u) [CommSemiring R] (S : Type u_1) [Semiring S] [Algebra R S] {ι₁ : Type v₁} {ι₂ : Type v₂} [DecidableEq ι₁] [DecidableEq ι₂] (M₁ : ι₁ → Type w₁) (M₂ : ι₂ → Type w₂) [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] [(i₁ : ι₁) → Module S (M₁ i₁)] [∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] : TensorProduct R (DirectSum ι₁ fun i₁ => M₁ i₁) (DirectSum ι₂ fun i₂ => M₂ i₂) ≃ₗ[S] DirectSum (ι₁ × ι₂) fun i => TensorProduct R (M₁ i.1) (M₂ i.2) - TensorProduct.directSum_lof_tmul_lof 📋 Mathlib.LinearAlgebra.DirectSum.TensorProduct
(R : Type u) [CommSemiring R] (S : Type u_1) [Semiring S] [Algebra R S] {ι₁ : Type v₁} {ι₂ : Type v₂} [DecidableEq ι₁] [DecidableEq ι₂] {M₁ : ι₁ → Type w₁} {M₂ : ι₂ → Type w₂} [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] [(i₁ : ι₁) → Module S (M₁ i₁)] [∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) : (TensorProduct.directSum R S M₁ M₂) ((DirectSum.lof S ι₁ M₁ i₁) m₁ ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i₂) m₂) = (DirectSum.lof S (ι₁ × ι₂) (fun i => TensorProduct R (M₁ i.1) (M₂ i.2)) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂) - TensorProduct.directSum_symm_lof_tmul 📋 Mathlib.LinearAlgebra.DirectSum.TensorProduct
(R : Type u) [CommSemiring R] (S : Type u_1) [Semiring S] [Algebra R S] {ι₁ : Type v₁} {ι₂ : Type v₂} [DecidableEq ι₁] [DecidableEq ι₂] {M₁ : ι₁ → Type w₁} {M₂ : ι₂ → Type w₂} [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] [(i₁ : ι₁) → Module S (M₁ i₁)] [∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) : (TensorProduct.directSum R S M₁ M₂).symm ((DirectSum.lof S (ι₁ × ι₂) (fun i => TensorProduct R (M₁ i.1) (M₂ i.2)) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)) = (DirectSum.lof S ι₁ M₁ i₁) m₁ ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i₂) m₂ - TensorProduct.directSum.eq_1 📋 Mathlib.LinearAlgebra.DirectSum.TensorProduct
(R : Type u) [CommSemiring R] (S : Type u_1) [Semiring S] [Algebra R S] {ι₁ : Type v₁} {ι₂ : Type v₂} [DecidableEq ι₁] [DecidableEq ι₂] (M₁ : ι₁ → Type w₁) (M₂ : ι₂ → Type w₂) [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] [(i₁ : ι₁) → Module S (M₁ i₁)] [∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] : TensorProduct.directSum R S M₁ M₂ = LinearEquiv.ofLinear (TensorProduct.AlgebraTensorModule.lift (DirectSum.toModule S ι₁ ((DirectSum ι₂ fun i₂ => M₂ i₂) →ₗ[R] DirectSum (ι₁ × ι₂) fun i => TensorProduct R (M₁ i.1) (M₂ i.2)) fun i₁ => (DirectSum.toModule R ι₂ (M₁ i₁ →ₗ[S] DirectSum (ι₁ × ι₂) fun i => TensorProduct R (M₁ i.1) (M₂ i.2)) fun i₂ => (TensorProduct.AlgebraTensorModule.curry (DirectSum.lof S (ι₁ × ι₂) (fun i => TensorProduct R (M₁ i.1) (M₂ i.2)) (i₁, i₂))).flip).flip)) (DirectSum.toModule S (ι₁ × ι₂) (TensorProduct R (DirectSum ι₁ fun i₁ => M₁ i₁) (DirectSum ι₂ fun i₂ => M₂ i₂)) fun i => TensorProduct.AlgebraTensorModule.map (DirectSum.lof S ι₁ M₁ i.1) (DirectSum.lof R ι₂ M₂ i.2)) ⋯ ⋯ - finsuppTensorFinsuppLid 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid N] [Module R N] : TensorProduct R (ι →₀ R) (κ →₀ N) ≃ₗ[R] ι × κ →₀ N - finsuppTensorFinsuppRid 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] : TensorProduct R (ι →₀ M) (κ →₀ R) ≃ₗ[R] ι × κ →₀ M - finsuppTensorFinsupp' 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] : TensorProduct R (ι →₀ R) (κ →₀ R) ≃ₗ[R] ι × κ →₀ R - finsuppTensorFinsupp'.eq_1 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] : finsuppTensorFinsupp' R ι κ = finsuppTensorFinsuppLid R R ι κ - finsuppTensorFinsuppLid_self 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] : finsuppTensorFinsuppLid R R ι κ = finsuppTensorFinsupp' R ι κ - finsuppTensorFinsuppRid_self 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] : finsuppTensorFinsuppRid R R ι κ = finsuppTensorFinsupp' R ι κ - finsuppTensorFinsupp 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] : TensorProduct R (ι →₀ M) (κ →₀ N) ≃ₗ[S] ι × κ →₀ TensorProduct R M N - finsuppTensorFinsuppRid.eq_1 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] : finsuppTensorFinsuppRid R M ι κ = (finsuppTensorFinsupp R R M R ι κ).trans (Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.rid R M)) - finsuppTensorFinsuppLid.eq_1 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid N] [Module R N] : finsuppTensorFinsuppLid R N ι κ = (finsuppTensorFinsupp R R R N ι κ).trans (Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.lid R N)) - finsuppTensorFinsuppLid_single_tmul_single 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid N] [Module R N] (a : ι) (b : κ) (r : R) (n : N) : (finsuppTensorFinsuppLid R N ι κ) ((fun₀ | a => r) ⊗ₜ[R] fun₀ | b => n) = fun₀ | (a, b) => r • n - finsuppTensorFinsuppRid_single_tmul_single 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : ι) (b : κ) (m : M) (r : R) : (finsuppTensorFinsuppRid R M ι κ) ((fun₀ | a => m) ⊗ₜ[R] fun₀ | b => r) = fun₀ | (a, b) => r • m - finsuppTensorFinsuppLid_apply_apply 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid N] [Module R N] (f : ι →₀ R) (g : κ →₀ N) (a : ι) (b : κ) : ((finsuppTensorFinsuppLid R N ι κ) (f ⊗ₜ[R] g)) (a, b) = f a • g b - finsuppTensorFinsuppRid_apply_apply 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] (f : ι →₀ M) (g : κ →₀ R) (a : ι) (b : κ) : ((finsuppTensorFinsuppRid R M ι κ) (f ⊗ₜ[R] g)) (a, b) = g b • f a - finsuppTensorFinsupp_single 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] (i : ι) (m : M) (k : κ) (n : N) : (finsuppTensorFinsupp R S M N ι κ) ((fun₀ | i => m) ⊗ₜ[R] fun₀ | k => n) = fun₀ | (i, k) => m ⊗ₜ[R] n - finsuppTensorFinsupp_apply 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] (f : ι →₀ M) (g : κ →₀ N) (i : ι) (k : κ) : ((finsuppTensorFinsupp R S M N ι κ) (f ⊗ₜ[R] g)) (i, k) = f i ⊗ₜ[R] g k - finsuppTensorFinsuppLid_symm_single_smul 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid N] [Module R N] (i : ι × κ) (r : R) (n : N) : ((finsuppTensorFinsuppLid R N ι κ).symm fun₀ | i => r • n) = (fun₀ | i.1 => r) ⊗ₜ[R] fun₀ | i.2 => n - finsuppTensorFinsuppRid_symm_single_smul 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] (i : ι × κ) (m : M) (r : R) : ((finsuppTensorFinsuppRid R M ι κ).symm fun₀ | i => r • m) = (fun₀ | i.1 => m) ⊗ₜ[R] fun₀ | i.2 => r - finsuppTensorFinsupp'_single_tmul_single 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] (a : ι) (b : κ) (r₁ r₂ : R) : (finsuppTensorFinsupp' R ι κ) ((fun₀ | a => r₁) ⊗ₜ[R] fun₀ | b => r₂) = fun₀ | (a, b) => r₁ * r₂ - finsuppTensorFinsupp'_apply_apply 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] (f : ι →₀ R) (g : κ →₀ R) (a : ι) (b : κ) : ((finsuppTensorFinsupp' R ι κ) (f ⊗ₜ[R] g)) (a, b) = f a * g b - finsuppTensorFinsupp_symm_single 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] (i : ι × κ) (m : M) (n : N) : ((finsuppTensorFinsupp R S M N ι κ).symm fun₀ | i => m ⊗ₜ[R] n) = (fun₀ | i.1 => m) ⊗ₜ[R] fun₀ | i.2 => n - finsuppTensorFinsupp.eq_1 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] : finsuppTensorFinsupp R S M N ι κ = TensorProduct.AlgebraTensorModule.congr (finsuppLEquivDirectSum S M ι) (finsuppLEquivDirectSum R N κ) ≪≫ₗ ((TensorProduct.directSum R S (fun x => M) fun x => N) ≪≫ₗ (finsuppLEquivDirectSum S (TensorProduct R M N) (ι × κ)).symm) - finsuppTensorFinsupp'_symm_single_eq_single_one_tmul 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] (i : ι × κ) (r : R) : ((finsuppTensorFinsupp' R ι κ).symm fun₀ | i => r) = (fun₀ | i.1 => 1) ⊗ₜ[R] fun₀ | i.2 => r - finsuppTensorFinsupp'_symm_single_eq_tmul_single_one 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] (i : ι × κ) (r : R) : ((finsuppTensorFinsupp' R ι κ).symm fun₀ | i => r) = (fun₀ | i.1 => r) ⊗ₜ[R] fun₀ | i.2 => 1 - finsuppTensorFinsupp'_symm_single_mul 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
(R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] (i : ι × κ) (r₁ r₂ : R) : ((finsuppTensorFinsupp' R ι κ).symm fun₀ | i => r₁ * r₂) = (fun₀ | i.1 => r₁) ⊗ₜ[R] fun₀ | i.2 => r₂ - Basis.tensorProduct 📋 Mathlib.LinearAlgebra.TensorProduct.Basis
{R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] (b : Basis ι S M) (c : Basis κ R N) : Basis (ι × κ) S (TensorProduct R M N) - 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.tensorProduct_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basis
{R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] (b : Basis ι S M) (c : Basis κ R N) (i : ι) (j : κ) : (b.tensorProduct c) (i, j) = b i ⊗ₜ[R] c j - Basis.tensorProduct_apply' 📋 Mathlib.LinearAlgebra.TensorProduct.Basis
{R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] (b : Basis ι S M) (c : Basis κ R N) (i : ι × κ) : (b.tensorProduct c) i = b i.1 ⊗ₜ[R] c i.2 - Basis.tensorProduct_repr_tmul_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basis
{R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] (b : Basis ι S M) (c : Basis κ R N) (m : M) (n : N) (i : ι) (j : κ) : ((b.tensorProduct c).repr (m ⊗ₜ[R] n)) (i, j) = (c.repr n) j • (b.repr m) i - Basis.tensorProduct.eq_1 📋 Mathlib.LinearAlgebra.TensorProduct.Basis
{R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] (b : Basis ι S M) (c : Basis κ R N) : b.tensorProduct c = Finsupp.basisSingleOne.map (TensorProduct.AlgebraTensorModule.congr b.repr c.repr ≪≫ₗ (finsuppTensorFinsupp R S S R ι κ ≪≫ₗ Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.AlgebraTensorModule.rid R S S))).symm - Algebra.TensorProduct.liftEquiv 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra S C] [Algebra R C] [IsScalarTower R S C] : { fg // ∀ (x : A) (y : B), Commute (fg.1 x) (fg.2 y) } ≃ (TensorProduct R A B →ₐ[S] C) - Algebra.TensorProduct.includeLeftRingHom_apply 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (a : A) : Algebra.TensorProduct.includeLeftRingHom a = a ⊗ₜ[R] 1 - Module.End.lTensorAlgHom_apply_apply 📋 Mathlib.RingTheory.TensorProduct.Basic
(R : Type u_1) (M : Type u_2) (N : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (a : Module.End R M) (a✝ : TensorProduct R N M) : ((Module.End.lTensorAlgHom R M N) a) a✝ = (TensorProduct.liftAux ((TensorProduct.mk R N M).compl₂ a)) a✝ - Module.End.rTensorAlgHom_apply_apply 📋 Mathlib.RingTheory.TensorProduct.Basic
(R : Type u_1) (M : Type u_2) (N : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (a : Module.End R M) (a✝ : TensorProduct R M N) : ((Module.End.rTensorAlgHom R M N) a) a✝ = (TensorProduct.liftAux (TensorProduct.mk R M N ∘ₗ a)) a✝ - Algebra.TensorProduct.liftEquiv_apply 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra S C] [Algebra R C] [IsScalarTower R S C] (fg : { fg // ∀ (x : A) (y : B), Commute (fg.1 x) (fg.2 y) }) : Algebra.TensorProduct.liftEquiv fg = Algebra.TensorProduct.lift (↑fg).1 (↑fg).2 ⋯ - Algebra.TensorProduct.liftEquiv_symm_apply_coe 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra S C] [Algebra R C] [IsScalarTower R S C] (f' : TensorProduct R A B →ₐ[S] C) : ↑(Algebra.TensorProduct.liftEquiv.symm f') = (f'.comp Algebra.TensorProduct.includeLeft, (AlgHom.restrictScalars R f').comp Algebra.TensorProduct.includeRight) - TensorProduct.exists_finset 📋 Mathlib.LinearAlgebra.TensorProduct.Finiteness
{R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R M N) : ∃ S, x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2 - TensorProduct.exists_multiset 📋 Mathlib.LinearAlgebra.TensorProduct.Finiteness
{R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R M N) : ∃ S, x = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) S).sum - Prod.comul_comp_fst 📋 Mathlib.RingTheory.Coalgebra.Basic
(R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] : CoalgebraStruct.comul ∘ₗ LinearMap.fst R A B = TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ CoalgebraStruct.comul - Prod.comul_comp_snd 📋 Mathlib.RingTheory.Coalgebra.Basic
(R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] : CoalgebraStruct.comul ∘ₗ LinearMap.snd R A B = TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ CoalgebraStruct.comul - Prod.comul_comp_inl 📋 Mathlib.RingTheory.Coalgebra.Basic
(R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] : CoalgebraStruct.comul ∘ₗ LinearMap.inl R A B = TensorProduct.map (LinearMap.inl R A B) (LinearMap.inl R A B) ∘ₗ CoalgebraStruct.comul - Prod.comul_comp_inr 📋 Mathlib.RingTheory.Coalgebra.Basic
(R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] : CoalgebraStruct.comul ∘ₗ LinearMap.inr R A B = TensorProduct.map (LinearMap.inr R A B) (LinearMap.inr R A B) ∘ₗ CoalgebraStruct.comul - Prod.comul_apply 📋 Mathlib.RingTheory.Coalgebra.Basic
(R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] (r : A × B) : CoalgebraStruct.comul r = (TensorProduct.map (LinearMap.inl R A B) (LinearMap.inl R A B)) (CoalgebraStruct.comul r.1) + (TensorProduct.map (LinearMap.inr R A B) (LinearMap.inr R A B)) (CoalgebraStruct.comul r.2) - Bialgebra.comulAlgHom_apply 📋 Mathlib.RingTheory.Bialgebra.Basic
(R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Bialgebra R A] (a : A) : (Bialgebra.comulAlgHom R A) a = CoalgebraStruct.comul a - TensorProduct.dualDistribEquivOfBasis_symm_apply 📋 Mathlib.LinearAlgebra.Dual.Lemmas
{R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (b : Basis ι R M) (c : Basis κ R N) (a : Module.Dual R (TensorProduct R M N)) : (TensorProduct.dualDistribEquivOfBasis b c).symm a = ∑ x, ∑ x_1, a (b x ⊗ₜ[R] c x_1) • b.coord x ⊗ₜ[R] c.coord x_1 - dualTensorHom_prodMap_zero 📋 Mathlib.LinearAlgebra.Contraction
{R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : Module.Dual R M) (p : P) : ((dualTensorHom R M P) (f ⊗ₜ[R] p)).prodMap 0 = (dualTensorHom R (M × N) (P × Q)) ((f ∘ₗ LinearMap.fst R M N) ⊗ₜ[R] (LinearMap.inl R P Q) p) - zero_prodMap_dualTensorHom 📋 Mathlib.LinearAlgebra.Contraction
{R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : Module.Dual R N) (q : Q) : LinearMap.prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) = (dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ LinearMap.snd R M N) ⊗ₜ[R] (LinearMap.inr R P Q) q) - CharacterModule.homEquiv_apply_apply 📋 Mathlib.Algebra.Module.CharacterModule
{R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] (c : A →ₗ[R] CharacterModule B) (x : (addConGen (TensorProduct.Eqv R A B)).Quotient) : (CharacterModule.homEquiv c) x = AddCon.liftOn x ⇑(FreeAddMonoid.lift fun mn => (c.toAddMonoidHom mn.1) mn.2) ⋯ - KaehlerDifferential.kerToTensor_apply 📋 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] (x : ↥(RingHom.ker (algebraMap A B))) : (KaehlerDifferential.kerToTensor R A B) x = 1 ⊗ₜ[A] (KaehlerDifferential.D R A) ↑x - Matrix.kroneckerTMul 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] : Matrix l m α → Matrix n p β → Matrix (l × n) (m × p) (TensorProduct R α β) - Matrix.kroneckerTMul.eq_1 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] : Matrix.kroneckerTMul R = Matrix.kroneckerMap fun x1 x2 => x1 ⊗ₜ[R] x2 - Matrix.trace_kroneckerTMul 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_3} {β : Type u_5} {m : Type u_10} {n : Type u_11} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [Fintype m] [Fintype n] (A : Matrix m m α) (B : Matrix n n β) : (Matrix.kroneckerMap (TensorProduct.tmul R) A B).trace = A.trace ⊗ₜ[R] B.trace - Matrix.kroneckerTMul_diagonal 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [DecidableEq n] (A : Matrix l m α) (b : n → β) : Matrix.kroneckerMap (TensorProduct.tmul R) A (Matrix.diagonal b) = Matrix.blockDiagonal fun i => A.map fun a => a ⊗ₜ[R] b i - Matrix.diagonal_kroneckerTMul_diagonal 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_3} {β : Type u_5} {m : Type u_10} {n : Type u_11} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [DecidableEq m] [DecidableEq n] (a : m → α) (b : n → β) : Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.diagonal a) (Matrix.diagonal b) = Matrix.diagonal fun mn => a mn.1 ⊗ₜ[R] b mn.2 - Matrix.kroneckerTMul_zero 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (A : Matrix l m α) : Matrix.kroneckerMap (TensorProduct.tmul R) A 0 = 0 - Matrix.zero_kroneckerTMul 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (B : Matrix n p β) : Matrix.kroneckerMap (TensorProduct.tmul R) 0 B = 0 - Matrix.single_kroneckerTMul_single 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (i₁ : l) (j₁ : m) (i₂ : n) (j₂ : p) (a : α) (b : β) : Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.single i₁ j₁ a) (Matrix.single i₂ j₂ b) = Matrix.single (i₁, i₂) (j₁, j₂) (a ⊗ₜ[R] b) - Matrix.stdBasisMatrix_kroneckerTMul_stdBasisMatrix 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (i₁ : l) (j₁ : m) (i₂ : n) (j₂ : p) (a : α) (b : β) : Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.single i₁ j₁ a) (Matrix.single i₂ j₂ b) = Matrix.single (i₁, i₂) (j₁, j₂) (a ⊗ₜ[R] b) - Matrix.add_kroneckerTMul 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [Module R α] (A₁ A₂ : Matrix l m α) (B : Matrix n p α) : Matrix.kroneckerMap (TensorProduct.tmul R) (A₁ + A₂) B = Matrix.kroneckerMap (fun x1 x2 => x1 ⊗ₜ[R] x2) A₁ B + Matrix.kroneckerMap (fun x1 x2 => x1 ⊗ₜ[R] x2) A₂ B - Matrix.kroneckerTMul_add 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (A : Matrix l m α) (B₁ B₂ : Matrix n p β) : Matrix.kroneckerMap (TensorProduct.tmul R) A (B₁ + B₂) = Matrix.kroneckerMap (fun x1 x2 => x1 ⊗ₜ[R] x2) A B₁ + Matrix.kroneckerMap (fun x1 x2 => x1 ⊗ₜ[R] x2) A B₂ - Matrix.smul_kroneckerTMul 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {S : Type u_2} {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [Monoid S] [DistribMulAction S α] [SMulCommClass R S α] (r : S) (A : Matrix l m α) (B : Matrix n p β) : Matrix.kroneckerMap (TensorProduct.tmul R) (r • A) B = r • Matrix.kroneckerMap (TensorProduct.tmul R) A B - Matrix.diagonal_kroneckerTMul 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [DecidableEq l] (a : l → α) (B : Matrix m n β) : Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.diagonal a) B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun i => B.map fun b => a i ⊗ₜ[R] b) - Matrix.one_kroneckerTMul_one 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_3} {m : Type u_10} {n : Type u_11} [CommSemiring R] [Semiring α] [Algebra R α] [DecidableEq m] [DecidableEq n] : Matrix.kroneckerMap (TensorProduct.tmul R) 1 1 = 1 - Matrix.det_kroneckerTMul 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_3} {β : Type u_5} {m : Type u_10} {n : Type u_11} [CommRing R] [CommRing α] [CommRing β] [Algebra R α] [Algebra R β] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A : Matrix m m α) (B : Matrix n n β) : (Matrix.kroneckerMap (TensorProduct.tmul R) A B).det = (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m) - Matrix.kroneckerTMul_smul 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {S : Type u_2} {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [Monoid S] [DistribMulAction S α] [DistribMulAction S β] [SMul S R] [SMulCommClass R S α] [IsScalarTower S R α] [IsScalarTower S R β] (r : S) (A : Matrix l m α) (B : Matrix n p β) : Matrix.kroneckerMap (TensorProduct.tmul R) A (r • B) = r • Matrix.kroneckerMap (TensorProduct.tmul R) A B - Matrix.mul_kroneckerTMul_mul 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {l' : Type u_15} {m' : Type u_16} {n' : Type u_17} [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] [Fintype m] [Fintype m'] (A : Matrix l m α) (B : Matrix m n α) (A' : Matrix l' m' β) (B' : Matrix m' n' β) : Matrix.kroneckerMap (TensorProduct.tmul R) (A * B) (A' * B') = Matrix.kroneckerMap (TensorProduct.tmul R) A A' * Matrix.kroneckerMap (TensorProduct.tmul R) B B' - Matrix.kroneckerTMulBilinear 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) (S : Type u_2) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [Semiring S] [Module S α] [SMulCommClass R S α] : Matrix l m α →ₗ[S] Matrix n p β →ₗ[R] Matrix (l × n) (m × p) (TensorProduct R α β) - Matrix.kroneckerTMul_assoc' 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} {q : Type u_13} {r : Type u_14} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [Module R α] [Module R β] [Module R γ] (A : Matrix l m α) (B : Matrix n p β) (C : Matrix q r γ) : ((Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.kroneckerMap (TensorProduct.tmul R) A B) C).map ⇑(TensorProduct.assoc R α β γ)).submatrix ⇑(Equiv.prodAssoc l n q).symm ⇑(Equiv.prodAssoc m p r).symm = Matrix.kroneckerMap (TensorProduct.tmul R) A (Matrix.kroneckerMap (TensorProduct.tmul R) B C) - Matrix.kroneckerTMulBilinear_apply 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {S : Type u_2} {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [Semiring S] [Module S α] [SMulCommClass R S α] (A : Matrix l m α) (B : Matrix n p β) : ((Matrix.kroneckerTMulBilinear R S) A) B = Matrix.kroneckerMap (TensorProduct.tmul R) A B - Matrix.kroneckerTMul_assoc 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} {q : Type u_13} {r : Type u_14} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [Module R α] [Module R β] [Module R γ] (A : Matrix l m α) (B : Matrix n p β) (C : Matrix q r γ) : (Matrix.reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r)) ((Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.kroneckerMap (TensorProduct.tmul R) A B) C).map ⇑(TensorProduct.assoc R α β γ)) = Matrix.kroneckerMap (TensorProduct.tmul R) A (Matrix.kroneckerMap (TensorProduct.tmul R) B C) - LinearIndependent.tmul_of_flat_left 📋 Mathlib.RingTheory.Flat.Basic
{R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {ι : Type u_6} {κ : Type u_7} {v : ι → M} {w : κ → N} [Module.Flat R M] (hv : LinearIndependent R v) (hw : LinearIndependent R w) : LinearIndependent R fun i => v i.1 ⊗ₜ[R] w i.2 - LinearIndependent.tmul_of_flat_right 📋 Mathlib.RingTheory.Flat.Basic
{R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {ι : Type u_6} {κ : Type u_7} {v : ι → M} {w : κ → N} [Module.Flat R N] (hv : LinearIndependent R v) (hw : LinearIndependent R w) : LinearIndependent R fun i => v i.1 ⊗ₜ[R] w i.2 - TensorProduct.LinearIndepOn.tmul_of_flat_left 📋 Mathlib.RingTheory.Flat.Basic
{R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {ι : Type u_6} {κ : Type u_7} {v : ι → M} {w : κ → N} {s : Set ι} {t : Set κ} [Module.Flat R M] (hv : LinearIndepOn R v s) (hw : LinearIndepOn R w t) : LinearIndepOn R (fun i => v i.1 ⊗ₜ[R] w i.2) (s ×ˢ t) - TensorProduct.LinearIndepOn.tmul_of_flat_right 📋 Mathlib.RingTheory.Flat.Basic
{R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {ι : Type u_6} {κ : Type u_7} {v : ι → M} {w : κ → N} {s : Set ι} {t : Set κ} [Module.Flat R N] (hv : LinearIndepOn R v s) (hw : LinearIndepOn R w t) : LinearIndepOn R (fun i => v i.1 ⊗ₜ[R] w i.2) (s ×ˢ t) - TensorProduct.prodRight 📋 Mathlib.LinearAlgebra.TensorProduct.Prod
(R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [CommSemiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Algebra R S] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] [Module R M₂] [Module R M₃] : TensorProduct R M₁ (M₂ × M₃) ≃ₗ[S] TensorProduct R M₁ M₂ × TensorProduct R M₁ M₃ - TensorProduct.prodLeft 📋 Mathlib.LinearAlgebra.TensorProduct.Prod
(R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [CommSemiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Algebra R S] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] [Module R M₂] [Module R M₃] [Module S M₂] [IsScalarTower R S M₂] : TensorProduct R (M₁ × M₂) M₃ ≃ₗ[S] TensorProduct R M₁ M₃ × TensorProduct R M₂ M₃ - TensorProduct.prodRight_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Prod
(R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [CommSemiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Algebra R S] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] [Module R M₂] [Module R M₃] (m₁ : M₁) (m : M₂ × M₃) : (TensorProduct.prodRight R S M₁ M₂ M₃) (m₁ ⊗ₜ[R] m) = (m₁ ⊗ₜ[R] m.1, m₁ ⊗ₜ[R] m.2) - TensorProduct.prodRight_symm_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Prod
(R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [CommSemiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Algebra R S] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] [Module R M₂] [Module R M₃] (m₁ : M₁) (m₂ : M₂) (m₃ : M₃) : (TensorProduct.prodRight R S M₁ M₂ M₃).symm (m₁ ⊗ₜ[R] m₂, m₁ ⊗ₜ[R] m₃) = m₁ ⊗ₜ[R] (m₂, m₃) - TensorProduct.prodLeft_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Prod
(R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [CommSemiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Algebra R S] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] [Module R M₂] [Module R M₃] [Module S M₂] [IsScalarTower R S M₂] (m₁ : M₁) (m₂ : M₂) (m₃ : M₃) : (TensorProduct.prodLeft R S M₁ M₂ M₃) ((m₁, m₂) ⊗ₜ[R] m₃) = (m₁ ⊗ₜ[R] m₃, m₂ ⊗ₜ[R] m₃) - TensorProduct.prodLeft_symm_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Prod
(R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [CommSemiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Algebra R S] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] [Module R M₂] [Module R M₃] [Module S M₂] [IsScalarTower R S M₂] (m₁ : M₁) (m₂ : M₂) (m₃ : M₃) : (TensorProduct.prodLeft R S M₁ M₂ M₃).symm (m₁ ⊗ₜ[R] m₃, m₂ ⊗ₜ[R] m₃) = (m₁, m₂) ⊗ₜ[R] m₃ - Algebra.TensorProduct.prodRight 📋 Mathlib.RingTheory.TensorProduct.Pi
(R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (B : Type u_6) (C : Type u_7) [Semiring B] [Semiring C] [Algebra R B] [Algebra R C] : TensorProduct R A (B × C) ≃ₐ[S] TensorProduct R A B × TensorProduct R A C - Algebra.TensorProduct.prodRight_tmul_fst 📋 Mathlib.RingTheory.TensorProduct.Pi
(R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (B : Type u_6) (C : Type u_7) [Semiring B] [Semiring C] [Algebra R B] [Algebra R C] (a : A) (x : B × C) : ((Algebra.TensorProduct.prodRight R S A B C) (a ⊗ₜ[R] x)).1 = a ⊗ₜ[R] x.1 - Algebra.TensorProduct.prodRight_tmul_snd 📋 Mathlib.RingTheory.TensorProduct.Pi
(R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (B : Type u_6) (C : Type u_7) [Semiring B] [Semiring C] [Algebra R B] [Algebra R C] (a : A) (x : B × C) : ((Algebra.TensorProduct.prodRight R S A B C) (a ⊗ₜ[R] x)).2 = a ⊗ₜ[R] x.2 - Algebra.TensorProduct.prodRight_tmul 📋 Mathlib.RingTheory.TensorProduct.Pi
(R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (B : Type u_6) (C : Type u_7) [Semiring B] [Semiring C] [Algebra R B] [Algebra R C] (a : A) (x : B × C) : (Algebra.TensorProduct.prodRight R S A B C) (a ⊗ₜ[R] x) = (a ⊗ₜ[R] x.1, a ⊗ₜ[R] x.2) - Algebra.TensorProduct.prodRight_symm_tmul 📋 Mathlib.RingTheory.TensorProduct.Pi
(R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (B : Type u_6) (C : Type u_7) [Semiring B] [Semiring C] [Algebra R B] [Algebra R C] (a : A) (b : B) (c : C) : (Algebra.TensorProduct.prodRight R S A B C).symm (a ⊗ₜ[R] b, a ⊗ₜ[R] c) = a ⊗ₜ[R] (b, c) - MatrixEquivTensor.invFun.eq_1 📋 Mathlib.RingTheory.MatrixAlgebra
(n : Type u_3) (R : Type u_5) (A : Type u_7) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] (M : Matrix n n A) : MatrixEquivTensor.invFun n R A M = ∑ p, M p.1 p.2 ⊗ₜ[R] Matrix.single p.1 p.2 1 - kroneckerTMulLinearEquiv 📋 Mathlib.RingTheory.MatrixAlgebra
(l : Type u_1) (m : Type u_2) (n : Type u_3) (p : Type u_4) (R : Type u_5) (S : Type u_6) (M : Type u_9) (N : Type u_10) [CommSemiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Algebra R S] [Module R M] [Module S M] [Module R N] [IsScalarTower R S M] [Fintype l] [Fintype m] [Fintype n] [Fintype p] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] : TensorProduct R (Matrix l m M) (Matrix n p N) ≃ₗ[S] Matrix (l × n) (m × p) (TensorProduct R M N) - Matrix.kroneckerTMulAlgEquiv 📋 Mathlib.RingTheory.MatrixAlgebra
(m : Type u_2) (n : Type u_3) (R : Type u_5) (S : Type u_6) (A : Type u_7) (B : Type u_8) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Fintype n] [DecidableEq n] [CommSemiring S] [Algebra R S] [Algebra S A] [IsScalarTower R S A] [Fintype m] [DecidableEq m] : TensorProduct R (Matrix m m A) (Matrix n n B) ≃ₐ[S] Matrix (m × n) (m × n) (TensorProduct R A B) - matrixEquivTensor_apply 📋 Mathlib.RingTheory.MatrixAlgebra
(n : Type u_3) (R : Type u_5) (A : Type u_7) [CommSemiring R] [Semiring A] [Algebra R A] [Fintype n] [DecidableEq n] (M : Matrix n n A) : (matrixEquivTensor n R A) M = ∑ p, M p.1 p.2 ⊗ₜ[R] Matrix.single p.1 p.2 1 - kroneckerTMulLinearEquiv_tmul 📋 Mathlib.RingTheory.MatrixAlgebra
(l : Type u_1) (m : Type u_2) (n : Type u_3) (p : Type u_4) (R : Type u_5) (S : Type u_6) (M : Type u_9) (N : Type u_10) [CommSemiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Algebra R S] [Module R M] [Module S M] [Module R N] [IsScalarTower R S M] [Fintype l] [Fintype m] [Fintype n] [Fintype p] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (a : Matrix l m M) (b : Matrix n p N) : (kroneckerTMulLinearEquiv l m n p R S M N) (a ⊗ₜ[R] b) = Matrix.kroneckerMap (fun x1 x2 => x1 ⊗ₜ[R] x2) a b - kroneckerTMulAlgEquiv_symm_single_tmul 📋 Mathlib.RingTheory.MatrixAlgebra
(l : Type u_1) (m : Type u_2) (n : Type u_3) (p : Type u_4) (R : Type u_5) (S : Type u_6) (M : Type u_9) (N : Type u_10) [CommSemiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Algebra R S] [Module R M] [Module S M] [Module R N] [IsScalarTower R S M] [Fintype l] [Fintype m] [Fintype n] [Fintype p] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (ia : l) (ja : m) (ib : n) (jb : p) (a : M) (b : N) : (kroneckerTMulLinearEquiv l m n p R S M N).symm (Matrix.single (ia, ib) (ja, jb) (a ⊗ₜ[R] b)) = Matrix.single ia ja a ⊗ₜ[R] Matrix.single ib jb b - kroneckerTMulAlgEquiv_symm_stdBasisMatrix_tmul 📋 Mathlib.RingTheory.MatrixAlgebra
(l : Type u_1) (m : Type u_2) (n : Type u_3) (p : Type u_4) (R : Type u_5) (S : Type u_6) (M : Type u_9) (N : Type u_10) [CommSemiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Algebra R S] [Module R M] [Module S M] [Module R N] [IsScalarTower R S M] [Fintype l] [Fintype m] [Fintype n] [Fintype p] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (ia : l) (ja : m) (ib : n) (jb : p) (a : M) (b : N) : (kroneckerTMulLinearEquiv l m n p R S M N).symm (Matrix.single (ia, ib) (ja, jb) (a ⊗ₜ[R] b)) = Matrix.single ia ja a ⊗ₜ[R] Matrix.single ib jb b - kroneckerTMulLinearEquiv_one 📋 Mathlib.RingTheory.MatrixAlgebra
(m : Type u_2) (n : Type u_3) (R : Type u_5) (S : Type u_6) (A : Type u_7) {B : Type u_8} [CommSemiring R] [Semiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra R A] [Algebra R B] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [Module S A] [IsScalarTower R S A] : (kroneckerTMulLinearEquiv m m n n R S A B) 1 = 1 - Matrix.kroneckerTMulAlgEquiv_apply 📋 Mathlib.RingTheory.MatrixAlgebra
{m : Type u_2} {n : Type u_3} (R : Type u_5) (S : Type u_6) {A : Type u_7} {B : Type u_8} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Fintype n] [DecidableEq n] [CommSemiring S] [Algebra R S] [Algebra S A] [IsScalarTower R S A] [Fintype m] [DecidableEq m] (x : TensorProduct R (Matrix m m A) (Matrix n n B)) : (Matrix.kroneckerTMulAlgEquiv m n R S A B) x = (kroneckerTMulLinearEquiv m m n n R S A B) x - Matrix.kroneckerTMulAlgEquiv_symm_apply 📋 Mathlib.RingTheory.MatrixAlgebra
{m : Type u_2} {n : Type u_3} (R : Type u_5) (S : Type u_6) {A : Type u_7} {B : Type u_8} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Fintype n] [DecidableEq n] [CommSemiring S] [Algebra R S] [Algebra S A] [IsScalarTower R S A] [Fintype m] [DecidableEq m] (x : Matrix (m × n) (m × n) (TensorProduct R A B)) : (Matrix.kroneckerTMulAlgEquiv m n R S A B).symm x = (kroneckerTMulLinearEquiv m m n n R S A B).symm x - kroneckerTMulLinearEquiv_mul 📋 Mathlib.RingTheory.MatrixAlgebra
(m : Type u_2) (n : Type u_3) (R : Type u_5) (S : Type u_6) (A : Type u_7) {B : Type u_8} [CommSemiring R] [Semiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra R A] [Algebra R B] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [Module S A] [IsScalarTower R S A] (x y : TensorProduct R (Matrix m m A) (Matrix n n B)) : (kroneckerTMulLinearEquiv m m n n R S A B) (x * y) = (kroneckerTMulLinearEquiv m m n n R S A B) x * (kroneckerTMulLinearEquiv m m n n R S A B) y - Algebra.TensorProduct.basisAux.eq_1 📋 Mathlib.RingTheory.TensorProduct.Free
{R : Type u_1} (A : Type u_2) {M : Type uM} {ι : Type uι} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Basis ι R M) : Algebra.TensorProduct.basisAux A b = (TensorProduct.congr (Finsupp.LinearEquiv.finsuppUnique R A PUnit.{uι + 1}).symm b.repr).trans ((finsuppTensorFinsupp R R A R PUnit.{uι + 1} ι).trans (Finsupp.lcongr (Equiv.uniqueProd ι PUnit.{uι + 1}) (TensorProduct.rid R A))) - 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 - Algebra.Generators.baseChange_val 📋 Mathlib.RingTheory.Extension.Generators
{R : Type u} {S : Type v} {ι : Type w} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_2} [CommRing T] [Algebra R T] (P : Algebra.Generators R S ι) (x : ι) : P.baseChange.val x = 1 ⊗ₜ[R] P.val x - Module.Presentation.tensor_G 📋 Mathlib.Algebra.Module.Presentation.Tensor
{A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] (pres₁ : Module.Presentation A M₁) (pres₂ : Module.Presentation A M₂) : (pres₁.tensor pres₂).G = (pres₁.G × pres₂.G) - Module.Presentation.tensor_R 📋 Mathlib.Algebra.Module.Presentation.Tensor
{A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] (pres₁ : Module.Presentation A M₁) (pres₂ : Module.Presentation A M₂) : (pres₁.tensor pres₂).R = (pres₁.R × pres₂.G ⊕ pres₁.G × pres₂.R) - Module.Relations.Solution.tensor_var 📋 Mathlib.Algebra.Module.Presentation.Tensor
{A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] {relations₁ : Module.Relations A} {relations₂ : Module.Relations A} (solution₁ : relations₁.Solution M₁) (solution₂ : relations₂.Solution M₂) (x✝ : (relations₁.tensor relations₂).G) : (solution₁.tensor solution₂).var x✝ = match x✝ with | (g₁, g₂) => solution₁.var g₁ ⊗ₜ[A] solution₂.var g₂ - Module.Presentation.tensor_var 📋 Mathlib.Algebra.Module.Presentation.Tensor
{A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] (pres₁ : Module.Presentation A M₁) (pres₂ : Module.Presentation A M₂) (x✝ : (pres₁.tensor pres₂.toRelations).G) : (pres₁.tensor pres₂).var x✝ = match x✝ with | (g₁, g₂) => pres₁.var g₁ ⊗ₜ[A] pres₂.var g₂ - Module.Presentation.tensor_relation 📋 Mathlib.Algebra.Module.Presentation.Tensor
{A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] (pres₁ : Module.Presentation A M₁) (pres₂ : Module.Presentation A M₂) (x✝ : pres₁.R × pres₂.G ⊕ pres₁.G × pres₂.R) : (pres₁.tensor pres₂).relation x✝ = match x✝ with | Sum.inl (r₁, g₂) => Finsupp.embDomain (Function.Embedding.sectL pres₁.G g₂) (pres₁.relation r₁) | Sum.inr (g₁, r₂) => Finsupp.embDomain (Function.Embedding.sectR g₁ pres₂.G) (pres₂.relation r₂) - PrimeSpectrum.tensorProductTo 📋 Mathlib.RingTheory.Spectrum.Prime.TensorProduct
(R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] (x : PrimeSpectrum (TensorProduct R S T)) : PrimeSpectrum S × PrimeSpectrum T - PrimeSpectrum.continuous_tensorProductTo 📋 Mathlib.RingTheory.Spectrum.Prime.TensorProduct
(R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] : Continuous (PrimeSpectrum.tensorProductTo R S T) - PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks 📋 Mathlib.RingTheory.Spectrum.Prime.TensorProduct
(R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] (hRT : (algebraMap R T).SurjectiveOnStalks) : Topology.IsEmbedding (PrimeSpectrum.tensorProductTo R S T) - PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks 📋 Mathlib.RingTheory.Spectrum.Prime.TensorProduct
(R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] (hRT : (algebraMap R T).SurjectiveOnStalks) : Topology.IsEmbedding (PrimeSpectrum.tensorProductTo R S T) - PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux 📋 Mathlib.RingTheory.Spectrum.Prime.TensorProduct
(R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] (hRT : (algebraMap R T).SurjectiveOnStalks) (p₁ p₂ : PrimeSpectrum (TensorProduct R S T)) (h : PrimeSpectrum.tensorProductTo R S T p₁ = PrimeSpectrum.tensorProductTo R S T p₂) : p₁ ≤ p₂ - Algebra.Generators.CotangentSpace.compEquiv 📋 Mathlib.RingTheory.Kaehler.JacobiZariski
{R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ) : (Q.comp P).toExtension.CotangentSpace ≃ₗ[T] Q.toExtension.CotangentSpace × TensorProduct S T P.toExtension.CotangentSpace - Algebra.Generators.CotangentSpace.fst_compEquiv 📋 Mathlib.RingTheory.Kaehler.JacobiZariski
{R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ) : LinearMap.fst T Q.toExtension.CotangentSpace (TensorProduct S T P.toExtension.CotangentSpace) ∘ₗ ↑(Algebra.Generators.CotangentSpace.compEquiv Q P) = Algebra.Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom - Algebra.Generators.CotangentSpace.compEquiv.eq_1 📋 Mathlib.RingTheory.Kaehler.JacobiZariski
{R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ) : Algebra.Generators.CotangentSpace.compEquiv Q P = (Q.comp P).cotangentSpaceBasis.repr.trans (Q.cotangentSpaceBasis.prod (Basis.baseChange T P.cotangentSpaceBasis)).repr.symm - Algebra.Generators.CotangentSpace.fst_compEquiv_apply 📋 Mathlib.RingTheory.Kaehler.JacobiZariski
{R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ) (x : (Q.comp P).toExtension.CotangentSpace) : ((Algebra.Generators.CotangentSpace.compEquiv Q P) x).1 = (Algebra.Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) x - Algebra.Generators.H1Cotangent.δAux_ofComp 📋 Mathlib.RingTheory.Kaehler.JacobiZariski
{R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ) (x : (Q.comp P).Ring) : (Algebra.Generators.H1Cotangent.δAux R Q) ((Q.ofComp P).toAlgHom x) = (LinearMap.baseChange T P.toExtension.toKaehler) ((Algebra.Generators.CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (KaehlerDifferential.D R (Q.comp P).Ring) x)).2 - Algebra.Generators.CotangentSpace.compEquiv_symm_inr 📋 Mathlib.RingTheory.Kaehler.JacobiZariski
{R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ) : ↑(Algebra.Generators.CotangentSpace.compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (TensorProduct S T P.toExtension.CotangentSpace) = LinearMap.liftBaseChange T (Algebra.Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) - Algebra.Generators.CotangentSpace.compEquiv_symm_zero 📋 Mathlib.RingTheory.Kaehler.JacobiZariski
{R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ) (x : TensorProduct S T P.toExtension.CotangentSpace) : (Algebra.Generators.CotangentSpace.compEquiv Q P).symm (0, x) = (LinearMap.liftBaseChange T (Algebra.Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) x - MultilinearMap.domCoprod_apply 📋 Mathlib.LinearAlgebra.Multilinear.TensorProduct
{R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [CommSemiring R] {N₁ : Type u_6} [AddCommMonoid N₁] [Module R N₁] {N₂ : Type u_7} [AddCommMonoid N₂] [Module R N₂] {N : Type u_8} [AddCommMonoid N] [Module R N] (a : MultilinearMap R (fun x => N) N₁) (b : MultilinearMap R (fun x => N) N₂) (v : (i : ι₁ ⊕ ι₂) → (fun x => N) i) : (a.domCoprod b) v = (a fun i₁ => v (Sum.inl i₁)) ⊗ₜ[R] b fun i₂ => v (Sum.inr i₂) - MultilinearMap.domCoprodDep_apply 📋 Mathlib.LinearAlgebra.Multilinear.TensorProduct
{R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [CommSemiring R] {N₁ : Type u_6} [AddCommMonoid N₁] [Module R N₁] {N₂ : Type u_7} [AddCommMonoid N₂] [Module R N₂] {N : ι₁ ⊕ ι₂ → Type u_8} [(i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)] [(i : ι₁ ⊕ ι₂) → Module R (N i)] (a : MultilinearMap R (fun i₁ => N (Sum.inl i₁)) N₁) (b : MultilinearMap R (fun i₂ => N (Sum.inr i₂)) N₂) (v : (i : ι₁ ⊕ ι₂) → N i) : (a.domCoprodDep b) v = (a fun i₁ => v (Sum.inl i₁)) ⊗ₜ[R] b fun i₂ => v (Sum.inr i₂) - AlternatingMap.domCoprod.summand_eq_zero_of_smul_invariant 📋 Mathlib.LinearAlgebra.Alternating.DomCoprod
{ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Equiv.Perm.ModSumCongr ιa ιb) {v : ιa ⊕ ιb → Mᵢ} {i j : ιa ⊕ ιb} (hv : v i = v j) (hij : i ≠ j) : Equiv.swap i j • σ = σ → (AlternatingMap.domCoprod.summand a b σ) v = 0 - AlternatingMap.domCoprod_coe 📋 Mathlib.LinearAlgebra.Alternating.DomCoprod
{ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) : ↑(a.domCoprod b) = ∑ σ, AlternatingMap.domCoprod.summand a b σ - AlternatingMap.domCoprod.summand_add_swap_smul_eq_zero 📋 Mathlib.LinearAlgebra.Alternating.DomCoprod
{ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Equiv.Perm.ModSumCongr ιa ιb) {v : ιa ⊕ ιb → Mᵢ} {i j : ιa ⊕ ιb} (hv : v i = v j) (hij : i ≠ j) : (AlternatingMap.domCoprod.summand a b σ) v + (AlternatingMap.domCoprod.summand a b (Equiv.swap i j • σ)) v = 0 - AlternatingMap.domCoprod_apply 📋 Mathlib.LinearAlgebra.Alternating.DomCoprod
{ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (v : ιa ⊕ ιb → Mᵢ) : (a.domCoprod b) v = (∑ σ, AlternatingMap.domCoprod.summand a b σ) v - AlternatingMap.domCoprod.summand_mk'' 📋 Mathlib.LinearAlgebra.Alternating.DomCoprod
{ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Equiv.Perm (ιa ⊕ ιb)) : AlternatingMap.domCoprod.summand a b (Quotient.mk'' σ) = Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b) - AlternatingMap.domCoprod.summand.eq_1 📋 Mathlib.LinearAlgebra.Alternating.DomCoprod
{ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Equiv.Perm.ModSumCongr ιa ιb) : AlternatingMap.domCoprod.summand a b σ = Quotient.liftOn' σ (fun σ => Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)) ⋯ - CliffordAlgebra.equivBaseChange_apply 📋 Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
{R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) : (CliffordAlgebra.equivBaseChange A Q) a = (CliffordAlgebra.toBaseChange A Q) a - TensorProduct.instModuleFstSnd 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.External
{R : Type u_1} {ι : Type u_2} (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] (i : ι × ι) : Module R (TensorProduct R (𝒜 i.1) (ℬ i.2)) - TensorProduct.gradedCommAux 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.External
(R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] : (DirectSum (ι × ι) fun i => TensorProduct R (𝒜 i.1) (ℬ i.2)) →ₗ[R] DirectSum (ι × ι) fun i => TensorProduct R (ℬ i.1) (𝒜 i.2) - TensorProduct.gradedCommAux_comp_gradedCommAux 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.External
(R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] : TensorProduct.gradedCommAux R 𝒜 ℬ ∘ₗ TensorProduct.gradedCommAux R ℬ 𝒜 = LinearMap.id - TensorProduct.gradedComm.eq_1 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.External
(R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] : TensorProduct.gradedComm R 𝒜 ℬ = ((TensorProduct.directSum R R 𝒜 ℬ).trans (LinearEquiv.ofLinear (TensorProduct.gradedCommAux R 𝒜 ℬ) (TensorProduct.gradedCommAux R ℬ 𝒜) ⋯ ⋯)).trans (TensorProduct.directSum R R ℬ 𝒜).symm - TensorProduct.gradedCommAux_lof_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.External
(R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] (i j : ι) (a : 𝒜 i) (b : ℬ j) : (TensorProduct.gradedCommAux R 𝒜 ℬ) ((DirectSum.lof R (ι × ι) (fun i => TensorProduct R (𝒜 i.1) (ℬ i.2)) (i, j)) (a ⊗ₜ[R] b)) = (-1) ^ (j * i) • (DirectSum.lof R (ι × ι) (fun i => TensorProduct R (ℬ i.1) (𝒜 i.2)) (j, i)) (b ⊗ₜ[R] a) - TensorProduct.gradedCommAux.eq_1 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.External
(R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] : TensorProduct.gradedCommAux R 𝒜 ℬ = DirectSum.toModule R (ι × ι) (DirectSum (ι × ι) fun i => TensorProduct R (ℬ i.1) (𝒜 i.2)) fun i => have o := DirectSum.lof R (ι × ι) (fun i => TensorProduct R (ℬ i.1) (𝒜 i.2)) i.swap; have s := (-1) ^ (i.1 * i.2); (s • o) ∘ₗ ↑(TensorProduct.comm R (𝒜 i.1) (ℬ i.2)) - TensorProduct.toMatrix_comm 📋 Mathlib.LinearAlgebra.TensorProduct.Matrix
{R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_7} {κ : Type u_8} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (bM : Basis ι R M) (bN : Basis κ R N) : (LinearMap.toMatrix (bM.tensorProduct bN) (bN.tensorProduct bM)) ↑(TensorProduct.comm R M N) = Matrix.submatrix 1 Prod.swap id - Matrix.toLin_kronecker 📋 Mathlib.LinearAlgebra.TensorProduct.Matrix
{R : Type u_1} {M : Type u_2} {N : Type u_3} {M' : Type u_5} {N' : Type u_6} {ι : Type u_7} {κ : Type u_8} {ι' : Type u_10} {κ' : Type u_11} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [Finite ι'] [Finite κ'] [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup M'] [AddCommGroup N'] [Module R M] [Module R N] [Module R M'] [Module R N'] (bM : Basis ι R M) (bN : Basis κ R N) (bM' : Basis ι' R M') (bN' : Basis κ' R N') (A : Matrix ι' ι R) (B : Matrix κ' κ R) : (Matrix.toLin (bM.tensorProduct bN) (bM'.tensorProduct bN')) (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A B) = TensorProduct.map ((Matrix.toLin bM bM') A) ((Matrix.toLin bN bN') B) - TensorProduct.toMatrix_map 📋 Mathlib.LinearAlgebra.TensorProduct.Matrix
{R : Type u_1} {M : Type u_2} {N : Type u_3} {M' : Type u_5} {N' : Type u_6} {ι : Type u_7} {κ : Type u_8} {ι' : Type u_10} {κ' : Type u_11} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [Finite ι'] [Finite κ'] [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup M'] [AddCommGroup N'] [Module R M] [Module R N] [Module R M'] [Module R N'] (bM : Basis ι R M) (bN : Basis κ R N) (bM' : Basis ι' R M') (bN' : Basis κ' R N') (f : M →ₗ[R] M') (g : N →ₗ[R] N') : (LinearMap.toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN')) (TensorProduct.map f g) = Matrix.kroneckerMap (fun x1 x2 => x1 * x2) ((LinearMap.toMatrix bM bM') f) ((LinearMap.toMatrix bN bN') g) - TensorProduct.toMatrix_assoc 📋 Mathlib.LinearAlgebra.TensorProduct.Matrix
{R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} {ι : Type u_7} {κ : Type u_8} {τ : Type u_9} [DecidableEq ι] [DecidableEq κ] [DecidableEq τ] [Fintype ι] [Fintype κ] [Fintype τ] [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (bM : Basis ι R M) (bN : Basis κ R N) (bP : Basis τ R P) : (LinearMap.toMatrix ((bM.tensorProduct bN).tensorProduct bP) (bM.tensorProduct (bN.tensorProduct bP))) ↑(TensorProduct.assoc R M N P) = Matrix.submatrix 1 id ⇑(Equiv.prodAssoc ι κ τ) - Rep.linearization_μ_hom 📋 Mathlib.RepresentationTheory.Rep
{k G : Type u} [CommRing k] [Monoid G] (X Y : Action (Type u) G) : (CategoryTheory.Functor.LaxMonoidal.μ (Rep.linearization k G) X Y).hom = ModuleCat.ofHom ↑(finsuppTensorFinsupp' k X.V Y.V) - Rep.leftRegularTensorTrivialIsoFree.eq_1 📋 Mathlib.RepresentationTheory.Rep
(k G : Type u) [CommRing k] [Monoid G] (α : Type u) [DecidableEq α] : Rep.leftRegularTensorTrivialIsoFree k G α = Action.mkIso (((finsuppTensorFinsupp' k G α).trans (Finsupp.domLCongr (Equiv.prodComm G α))).trans (Finsupp.finsuppProdLEquiv k)).toModuleIso ⋯ - Rep.linearization_δ_hom 📋 Mathlib.RepresentationTheory.Rep
{k G : Type u} [CommRing k] [Monoid G] (X Y : Action (Type u) G) : (CategoryTheory.Functor.OplaxMonoidal.δ (Rep.linearization k G) X Y).hom = ModuleCat.ofHom ↑(finsuppTensorFinsupp' k X.V Y.V).symm - Rep.leftRegularTensorTrivialIsoFree_hom_hom 📋 Mathlib.RepresentationTheory.Rep
(k G : Type u) [CommRing k] [Monoid G] (α : Type u) [DecidableEq α] : (Rep.leftRegularTensorTrivialIsoFree k G α).hom.hom = ModuleCat.ofHom ↑(((finsuppTensorFinsupp' k G α).trans (Finsupp.domLCongr (Equiv.prodComm G α))).trans (Finsupp.finsuppProdLEquiv k)) - Rep.leftRegularTensorTrivialIsoFree_inv_hom 📋 Mathlib.RepresentationTheory.Rep
(k G : Type u) [CommRing k] [Monoid G] (α : Type u) [DecidableEq α] : (Rep.leftRegularTensorTrivialIsoFree k G α).inv.hom = ModuleCat.ofHom ↑((Finsupp.finsuppProdLEquiv k).symm.trans ((Finsupp.domLCongr (Equiv.prodComm α G)).trans (finsuppTensorFinsupp' k G α).symm)) - groupHomology.H1AddEquivOfIsTrivial_apply 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
{k G : Type u} [CommRing k] [Group G] (A : Rep k G) [DecidableEq G] [A.IsTrivial] (a✝ : ↑(groupHomology.H1 A)) : (groupHomology.H1AddEquivOfIsTrivial A) a✝ = (groupHomology.H1ToTensorOfIsTrivial A) a✝ - LinearIndependent.tmul_of_isDomain 📋 Mathlib.RingTheory.Flat.Domain
{R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {ι : Type u_6} {κ : Type u_7} {v : ι → M} {w : κ → N} (hv : LinearIndependent R v) (hw : LinearIndependent R w) : LinearIndependent R fun i => v i.1 ⊗ₜ[R] w i.2 - LinearIndepOn.tmul_of_isDomain 📋 Mathlib.RingTheory.Flat.Domain
{R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {ι : Type u_6} {κ : Type u_7} {v : ι → M} {w : κ → N} {s : Set ι} {t : Set κ} (hv : LinearIndepOn R v s) (hw : LinearIndepOn R w t) : LinearIndepOn R (fun i => v i.1 ⊗ₜ[R] w i.2) (s ×ˢ t) - KaehlerDifferential.tensorKaehlerEquiv_symm_apply 📋 Mathlib.RingTheory.Kaehler.TensorProduct
(R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] [h : Algebra.IsPushout R S A B] (a : Ω[B⁄S]) : (KaehlerDifferential.tensorKaehlerEquiv R S A B).symm a = (KaehlerDifferential.derivationTensorProduct R S A B).liftKaehlerDifferential a
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 ?aIf 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 ?bBy 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 findtsum_lt_tsumeven though the hypothesisf i < g iis 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 e086424 serving mathlib revision a390088