TensorProduct

📁 Source: Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean

Statistics

Metric	Count
Definitions baseChange, tensorDistrib, tmul, tensorDistrib, tmul	5
Theorems associated_baseChange, associated_tmul, baseChange_tmul, polarBilin_baseChange, polarBilin_tmul, tensorDistrib_tmul, associated_tmul, tensorDistrib_tmul, baseChange_ext, baseChange_ext_iff	10
Total	15

QuadraticForm

Definitions

Name	Category	Theorems
baseChange 📖	CompOp	17 math math: CliffordAlgebra.toBaseChange_reverse, CliffordAlgebra.equivBaseChange_symm_apply, CliffordAlgebra.ofBaseChange_toBaseChange, polarBilin_baseChange, CliffordAlgebra.toBaseChange_comp_ofBaseChange, CliffordAlgebra.toBaseChange_comp_involute, baseChange_tmul, CliffordAlgebra.ofBaseChange_tmul_ι, CliffordAlgebra.ofBaseChangeAux_ι, CliffordAlgebra.toBaseChange_ofBaseChange, CliffordAlgebra.toBaseChange_comp_reverseOp, CliffordAlgebra.equivBaseChange_apply, CliffordAlgebra.toBaseChange_involute, CliffordAlgebra.ofBaseChange_tmul_one, CliffordAlgebra.toBaseChange_ι, associated_baseChange, CliffordAlgebra.ofBaseChange_comp_toBaseChange
tensorDistrib 📖	CompOp	1 math math: tensorDistrib_tmul
tmul 📖	CompOp	32 math math: tmul_tensorMap_apply, tmul_comp_tensorComm, polarBilin_tmul, tensorRId_symm_apply, tensorAssoc_toLinearEquiv, QuadraticModuleCat.instMonoidalCategory.tensorObj_form, tensorRId_apply, comp_tensorLId_eq, tmul_tensorAssoc_apply, tmul_tensorComm_apply, tensorLId_toLinearEquiv, tmul_tensorRId_apply, tensorComm_toLinearEquiv, QuadraticModuleCat.toIsometry_hom_leftUnitor, QuadraticModuleCat.toIsometry_hom_rightUnitor, tensorLId_symm_apply, tensorComm_apply, tmul_comp_tensorMap, tensorAssoc_symm_apply, QuadraticModuleCat.toIsometry_inv_rightUnitor, tensorRId_toLinearEquiv, tmul_tensorLId_apply, tensorLId_apply, comp_tensorRId_eq, tensorAssoc_apply, QuadraticMap.Isometry.tmul_apply, QuadraticModuleCat.toIsometry_inv_leftUnitor, tmul_comp_tensorAssoc, associated_tmul, tensorComm_symm, QuadraticModuleCat.hom_hom_associator, QuadraticModuleCat.hom_inv_associator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associated_baseChange 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring QuadraticMap TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid Algebra.toModule TensorProduct.addCommGroup Ring.toAddCommGroup CommRing.toRing TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass LinearMap.BilinMap QuadraticMap.instAddCommMonoid LinearMap.addCommMonoid LinearMap.module QuadraticMap.instModuleOfSMulCommClass smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike QuadraticMap.associated QuadraticMap.instInvertibleEndOfNat baseChange LinearMap.BilinForm.baseChange	—	Nat.instAtLeastTwoHAddOfNat Algebra.to_smulCommClass smulCommClass_self LinearMap.instSMulCommClass IsScalarTower.right associated_tmul QuadraticMap.associated_sq
associated_tmul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring QuadraticMap TensorProduct AddCommGroup.toAddCommMonoid TensorProduct.addCommGroup TensorProduct.leftModule Ring.toAddCommGroup CommRing.toRing Semiring.toModule LinearMap.BilinMap QuadraticMap.instAddCommMonoid LinearMap.addCommMonoid LinearMap.module QuadraticMap.instModuleOfSMulCommClass smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike QuadraticMap.associated QuadraticMap.instInvertibleEndOfNat tmul LinearMap.BilinForm.tmul	—	Nat.instAtLeastTwoHAddOfNat smulCommClass_self LinearMap.instSMulCommClass LinearMap.BilinForm.tmul.eq_1 IsScalarTower.to_smulCommClass' IsScalarTower.right Algebra.to_smulCommClass LinearMap.BilinForm.tensorDistrib.eq_1 LinearMap.comp_apply LinearMap.BilinMap.tmul.eq_1 IsScalarTower.to_smulCommClass QuadraticMap.associated_tmul TensorProduct.AlgebraTensorModule.curry_injective LinearMap.instIsScalarTower IsScalarTower.left RingHomInvPair.ids LinearMap.ext tensorDistrib_tmul QuadraticMap.tensorDistrib_tmul map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass
baseChange_tmul 📖	mathematical	—	DFunLike.coe QuadraticForm TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid Algebra.toModule CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass QuadraticMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring baseChange TensorProduct.tmul Algebra.toSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Nat.instAtLeastTwoHAddOfNat tensorDistrib_tmul
polarBilin_baseChange 📖	mathematical	—	QuadraticMap.polarBilin TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid Algebra.toModule CommSemiring.toSemiring TensorProduct.addCommGroup Ring.toAddCommGroup CommRing.toRing TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass baseChange LinearMap.BilinForm.baseChange	—	Nat.instAtLeastTwoHAddOfNat Algebra.to_smulCommClass baseChange.eq_1 LinearMap.BilinForm.baseChange.eq_1 LinearMap.instSMulCommClass polarBilin_tmul LinearMap.BilinForm.tmul.eq_1 map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass TensorProduct.smul_tmul' IsScalarTower.to_smulCommClass IsScalarTower.right IsScalarTower.to_smulCommClass' QuadraticMap.two_nsmul_associated smulCommClass_self QuadraticMap.coe_associatedHom QuadraticMap.associated_sq SMulCommClass.smul_comm AddMonoid.nat_smulCommClass' smul_assoc AddCommMonoid.nat_isScalarTower two_smul invOf_two_add_invOf_two one_smul
polarBilin_tmul 📖	mathematical	—	QuadraticMap.polarBilin TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct.addCommGroup Ring.toAddCommGroup CommRing.toRing TensorProduct.leftModule CommSemiring.toSemiring Semiring.toModule tmul LinearMap.BilinMap TensorProduct.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring LinearMap.instSMul LinearMap RingHom.id LinearMap.addCommMonoid LinearMap.module DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid LinearMap.instDistribMulAction Module.toDistribMulAction NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass Invertible.invOf Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat LinearMap.BilinForm.tmul	—	Nat.instAtLeastTwoHAddOfNat Algebra.to_smulCommClass LinearMap.instSMulCommClass IsScalarTower.to_smulCommClass IsScalarTower.right IsScalarTower.to_smulCommClass' QuadraticMap.two_nsmul_associated LinearMap.BilinForm.tmul.congr_simp AddMonoid.nat_smulCommClass' TensorProduct.tmul_smul TensorProduct.CompatibleSMul.isScalarTower AddCommMonoid.nat_isScalarTower map_nsmul DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass smulCommClass_self associated_tmul SMulCommClass.smul_comm smul_assoc two_smul invOf_two_add_invOf_two one_smul
tensorDistrib_tmul 📖	mathematical	—	DFunLike.coe QuadraticForm TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring QuadraticMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule LinearMap RingHom.id QuadraticMap.instAddCommMonoid QuadraticMap.instModuleOfSMulCommClass Algebra.toModule Algebra.to_smulCommClass Algebra.id QuadraticMap.instSMulCommClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction LinearMap.instFunLike tensorDistrib TensorProduct.tmul Algebra.toSMul	—	Nat.instAtLeastTwoHAddOfNat IsScalarTower.to_smulCommClass' IsScalarTower.right LinearMap.instSMulCommClass Algebra.to_smulCommClass LinearMap.BilinForm.tensorDistrib_tmul QuadraticMap.associated_eq_self_apply

QuadraticMap

Definitions

Name	Category	Theorems
tensorDistrib 📖	CompOp	1 math math: tensorDistrib_tmul
tmul 📖	CompOp	1 math math: associated_tmul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associated_tmul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring QuadraticMap TensorProduct AddCommGroup.toAddCommMonoid TensorProduct.addCommGroup TensorProduct.leftModule IsScalarTower.to_smulCommClass LinearMap.BilinMap instAddCommMonoid LinearMap.addCommMonoid LinearMap.module instModuleOfSMulCommClass smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike associated instInvertibleEndOfNat tmul LinearMap.BilinMap.tmul	—	Nat.instAtLeastTwoHAddOfNat IsScalarTower.to_smulCommClass smulCommClass_self LinearMap.instSMulCommClass tmul.eq_1 LinearMap.BilinMap.tmul.eq_1 Invertible.subsingleton TensorProduct.isScalarTower_left IsScalarTower.left IsScalarTower.to_smulCommClass' MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_ofNat Lean.Meta.FastSubsingleton.elim associated_left_inverse LinearMap.BilinMap.tmul_isSymm associated_isSymm
tensorDistrib_tmul 📖	mathematical	—	DFunLike.coe QuadraticMap TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass instFunLike LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid instModuleOfSMulCommClass smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing instSMulCommClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero TensorProduct.smulCommClass_left LinearMap.instFunLike tensorDistrib TensorProduct.tmul	—	Nat.instAtLeastTwoHAddOfNat IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass smulCommClass_self TensorProduct.smulCommClass_left LinearMap.BilinMap.tensorDistrib_tmul associated_eq_self_apply

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange_ext 📖	—	DFunLike.coe QuadraticMap TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid Algebra.toModule CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass QuadraticMap.instFunLike TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—	Algebra.to_smulCommClass mul_one smul_eq_mul TensorProduct.smul_tmul' QuadraticMap.map_smul QuadraticMap.ext TensorProduct.induction_on map_zero QuadraticMap.zeroHomClass TensorProduct.AlgebraTensorModule.curry_injective IsScalarTower.right IsScalarTower.to_smulCommClass' LinearMap.instIsScalarTower LinearMap.ext_ring IsScalarTower.to_smulCommClass LinearMap.ext TensorProduct.tmul_add Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.sub_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.sub_eq_eval₁ Mathlib.Tactic.Module.NF.zero_sub_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval₁ Mathlib.Tactic.Module.NF.add_eq_eval₂ add_zero zero_add Mathlib.Tactic.Module.NF.add_eq_eval₃ Mathlib.Tactic.Module.NF.sub_eq_eval₂ Mathlib.Tactic.Module.NF.zero_eq_eval Mathlib.Tactic.Module.NF.eq_cons_const eq_natCast RingHom.instRingHomClass Nat.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr
baseChange_ext_iff 📖	mathematical	—	DFunLike.coe QuadraticMap TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid Algebra.toModule CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass QuadraticMap.instFunLike TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Algebra.to_smulCommClass baseChange_ext

---

← Back to Index