Isometries

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

Statistics

Metric	Count
Definitions `tensorAssoc`, `tensorComm`, `tensorLId`, `tensorRId`, `tmul`	5
Theorems `comp_tensorLId_eq`, `comp_tensorRId_eq`, `tensorAssoc_apply`, `tensorAssoc_symm_apply`, `tensorAssoc_toLinearEquiv`, `tensorComm_apply`, `tensorComm_symm`, `tensorComm_toLinearEquiv`, `tensorLId_apply`, `tensorLId_symm_apply`, `tensorLId_toLinearEquiv`, `tensorRId_apply`, `tensorRId_symm_apply`, `tensorRId_toLinearEquiv`, `tmul_comp_tensorAssoc`, `tmul_comp_tensorComm`, `tmul_comp_tensorMap`, `tmul_tensorAssoc_apply`, `tmul_tensorComm_apply`, `tmul_tensorLId_apply`, `tmul_tensorMap_apply`, `tmul_tensorRId_apply`, `tmul_apply`	23
Total	28

QuadraticForm

Definitions

Name	Category	Theorems
`tensorAssoc` 📖	CompOp	5 math math: `tensorAssoc_toLinearEquiv`, `tensorAssoc_symm_apply`, `tensorAssoc_apply`, `QuadraticModuleCat.hom_hom_associator`, `QuadraticModuleCat.hom_inv_associator`
`tensorComm` 📖	CompOp	3 math math: `tensorComm_toLinearEquiv`, `tensorComm_apply`, `tensorComm_symm`
`tensorLId` 📖	CompOp	5 math math: `tensorLId_toLinearEquiv`, `QuadraticModuleCat.toIsometry_hom_leftUnitor`, `tensorLId_symm_apply`, `tensorLId_apply`, `QuadraticModuleCat.toIsometry_inv_leftUnitor`
`tensorRId` 📖	CompOp	5 math math: `tensorRId_symm_apply`, `tensorRId_apply`, `QuadraticModuleCat.toIsometry_hom_rightUnitor`, `QuadraticModuleCat.toIsometry_inv_rightUnitor`, `tensorRId_toLinearEquiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_tensorLId_eq` 📖	mathematical	—	`QuadraticMap.comp` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Algebra.to_smulCommClass` `Algebra.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `LinearEquiv.toLinearMap` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.instModule` `TensorProduct.lid` `tmul` `IsScalarTower.right` `QuadraticMap.sq` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Nat.instAtLeastTwoHAddOfNat` `baseChange_ext` `IsScalarTower.right` `Algebra.to_smulCommClass` `RingHomInvPair.ids` `one_smul` `QuadraticMap.instSMulCommClass` `tensorDistrib_tmul` `mul_one`
`comp_tensorRId_eq` 📖	mathematical	—	`QuadraticMap.comp` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `LinearEquiv.toLinearMap` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.instModule` `TensorProduct.rid` `tmul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `QuadraticMap.sq` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.to_smulCommClass` `IsScalarTower.right`	—	`Nat.instAtLeastTwoHAddOfNat` `Function.RightInverse.injective` `smulCommClass_self` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `IsScalarTower.to_smulCommClass'` `LinearMap.instSMulCommClass` `QuadraticMap.associated_rightInverse` `RingHomInvPair.ids` `IsScalarTower.left` `Algebra.to_smulCommClass` `TensorProduct.AlgebraTensorModule.curry_injective` `LinearMap.instIsScalarTower` `LinearMap.ext` `LinearMap.ext_ring` `QuadraticMap.associated_comp` `associated_tmul` `one_smul` `LinearMap.BilinForm.tmul.congr_simp` `QuadraticMap.associated_sq` `mul_one` `one_mul`
`tensorAssoc_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.IsometryEquiv` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommGroup` `TensorProduct.instModule` `TensorProduct.leftModule` `CommSemiring.toSemiring` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `TensorProduct.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Semiring.toModule` `tmul` `Algebra.id` `TensorProduct.isScalarTower` `Algebra.toSMul` `IsScalarTower.left` `EquivLike.toFunLike` `QuadraticMap.IsometryEquiv.instEquivLike` `tensorAssoc` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `DFinsupp.instEquivLikeLinearEquiv` `TensorProduct.assoc`	—	`Nat.instAtLeastTwoHAddOfNat` `smulCommClass_self` `TensorProduct.smulCommClass_left` `TensorProduct.isScalarTower` `IsScalarTower.left`
`tensorAssoc_symm_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.IsometryEquiv` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommGroup` `TensorProduct.leftModule` `CommSemiring.toSemiring` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `TensorProduct.instModule` `TensorProduct.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Semiring.toModule` `tmul` `Algebra.id` `IsScalarTower.left` `TensorProduct.isScalarTower` `Algebra.toSMul` `EquivLike.toFunLike` `QuadraticMap.IsometryEquiv.instEquivLike` `QuadraticMap.IsometryEquiv.symm` `tensorAssoc` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `TensorProduct.assoc`	—	`Nat.instAtLeastTwoHAddOfNat` `smulCommClass_self` `TensorProduct.smulCommClass_left` `IsScalarTower.left` `TensorProduct.isScalarTower`
`tensorAssoc_toLinearEquiv` 📖	mathematical	—	`QuadraticMap.IsometryEquiv.toLinearEquiv` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommGroup` `TensorProduct.instModule` `TensorProduct.leftModule` `CommSemiring.toSemiring` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `TensorProduct.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Semiring.toModule` `tmul` `Algebra.id` `TensorProduct.isScalarTower` `Algebra.toSMul` `IsScalarTower.left` `tensorAssoc` `TensorProduct.assoc`	—	`Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `smulCommClass_self` `TensorProduct.smulCommClass_left` `TensorProduct.isScalarTower` `IsScalarTower.left`
`tensorComm_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.IsometryEquiv` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `TensorProduct.leftModule` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Semiring.toModule` `tmul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `EquivLike.toFunLike` `QuadraticMap.IsometryEquiv.instEquivLike` `tensorComm` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.instModule` `DFinsupp.instEquivLikeLinearEquiv` `TensorProduct.comm`	—	`Nat.instAtLeastTwoHAddOfNat` `smulCommClass_self` `IsScalarTower.left`
`tensorComm_symm` 📖	mathematical	—	`QuadraticMap.IsometryEquiv.symm` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `TensorProduct.leftModule` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Semiring.toModule` `tmul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `tensorComm`	—	`Nat.instAtLeastTwoHAddOfNat` `smulCommClass_self` `IsScalarTower.left`
`tensorComm_toLinearEquiv` 📖	mathematical	—	`QuadraticMap.IsometryEquiv.toLinearEquiv` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `TensorProduct.leftModule` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Semiring.toModule` `tmul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `tensorComm` `TensorProduct.comm`	—	`Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `smulCommClass_self` `IsScalarTower.left`
`tensorLId_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.IsometryEquiv` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct.leftModule` `Algebra.to_smulCommClass` `Algebra.id` `tmul` `IsScalarTower.right` `QuadraticMap.sq` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EquivLike.toFunLike` `QuadraticMap.IsometryEquiv.instEquivLike` `tensorLId` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.instModule` `DFinsupp.instEquivLikeLinearEquiv` `TensorProduct.lid`	—	`Nat.instAtLeastTwoHAddOfNat` `Algebra.to_smulCommClass` `IsScalarTower.right`
`tensorLId_symm_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.IsometryEquiv` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct.leftModule` `Algebra.to_smulCommClass` `Algebra.id` `tmul` `IsScalarTower.right` `QuadraticMap.sq` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EquivLike.toFunLike` `QuadraticMap.IsometryEquiv.instEquivLike` `QuadraticMap.IsometryEquiv.symm` `tensorLId` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.instModule` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `TensorProduct.lid`	—	`Nat.instAtLeastTwoHAddOfNat` `Algebra.to_smulCommClass` `IsScalarTower.right`
`tensorLId_toLinearEquiv` 📖	mathematical	—	`QuadraticMap.IsometryEquiv.toLinearEquiv` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct.leftModule` `Algebra.to_smulCommClass` `Algebra.id` `tmul` `IsScalarTower.right` `QuadraticMap.sq` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `tensorLId` `TensorProduct.lid`	—	`Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `IsScalarTower.right`
`tensorRId_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.IsometryEquiv` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct.leftModule` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `tmul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `QuadraticMap.sq` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.to_smulCommClass` `IsScalarTower.right` `EquivLike.toFunLike` `QuadraticMap.IsometryEquiv.instEquivLike` `tensorRId` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.instModule` `DFinsupp.instEquivLikeLinearEquiv` `TensorProduct.rid`	—	`Nat.instAtLeastTwoHAddOfNat` `smulCommClass_self` `IsScalarTower.left` `Algebra.to_smulCommClass` `IsScalarTower.right`
`tensorRId_symm_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.IsometryEquiv` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct.leftModule` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `tmul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `QuadraticMap.sq` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.to_smulCommClass` `IsScalarTower.right` `EquivLike.toFunLike` `QuadraticMap.IsometryEquiv.instEquivLike` `QuadraticMap.IsometryEquiv.symm` `tensorRId` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.instModule` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `TensorProduct.rid`	—	`Nat.instAtLeastTwoHAddOfNat` `smulCommClass_self` `IsScalarTower.left` `Algebra.to_smulCommClass` `IsScalarTower.right`
`tensorRId_toLinearEquiv` 📖	mathematical	—	`QuadraticMap.IsometryEquiv.toLinearEquiv` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct.leftModule` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `tmul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `QuadraticMap.sq` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.to_smulCommClass` `IsScalarTower.right` `tensorRId` `TensorProduct.rid`	—	`Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `smulCommClass_self` `IsScalarTower.left` `Algebra.to_smulCommClass` `IsScalarTower.right`
`tmul_comp_tensorAssoc` 📖	mathematical	—	`QuadraticMap.comp` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommGroup` `TensorProduct.instModule` `TensorProduct.leftModule` `CommSemiring.toSemiring` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `TensorProduct.addCommMonoid` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `tmul` `Algebra.id` `IsScalarTower.left` `LinearEquiv.toLinearMap` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.assoc` `TensorProduct.isScalarTower` `Algebra.toSMul`	—	`Nat.instAtLeastTwoHAddOfNat` `Function.RightInverse.injective` `smulCommClass_self` `TensorProduct.smulCommClass_left` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `IsScalarTower.to_smulCommClass'` `LinearMap.instSMulCommClass` `QuadraticMap.associated_rightInverse` `IsScalarTower.left` `RingHomInvPair.ids` `TensorProduct.isScalarTower` `TensorProduct.AlgebraTensorModule.curry_injective` `Algebra.to_smulCommClass` `LinearMap.instIsScalarTower` `LinearMap.ext` `QuadraticMap.associated_comp` `associated_tmul` `LinearMap.BilinForm.tmul.congr_simp` `mul_assoc`
`tmul_comp_tensorComm` 📖	mathematical	—	`QuadraticMap.comp` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `CommSemiring.toSemiring` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `tmul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LinearEquiv.toLinearMap` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.instModule` `TensorProduct.comm`	—	`Nat.instAtLeastTwoHAddOfNat` `Function.RightInverse.injective` `smulCommClass_self` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `IsScalarTower.to_smulCommClass'` `LinearMap.instSMulCommClass` `QuadraticMap.associated_rightInverse` `IsScalarTower.left` `RingHomInvPair.ids` `TensorProduct.AlgebraTensorModule.curry_injective` `Algebra.to_smulCommClass` `LinearMap.instIsScalarTower` `LinearMap.ext` `QuadraticMap.associated_comp` `associated_tmul` `mul_comm`
`tmul_comp_tensorMap` 📖	mathematical	—	`QuadraticMap.comp` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.leftModule` `CommSemiring.toSemiring` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `tmul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `TensorProduct.map` `RingHom.id` `QuadraticMap.Isometry.toLinearMap`	—	`Nat.instAtLeastTwoHAddOfNat` `QuadraticMap.ext` `QuadraticMap.Isometry.map_app` `Function.RightInverse.injective` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `IsScalarTower.to_smulCommClass'` `LinearMap.instSMulCommClass` `QuadraticMap.associated_rightInverse` `smulCommClass_self` `IsScalarTower.left` `TensorProduct.AlgebraTensorModule.curry_injective` `Algebra.to_smulCommClass` `LinearMap.instIsScalarTower` `LinearMap.ext` `QuadraticMap.associated_comp` `associated_tmul` `tmul.congr_simp` `LinearMap.BilinForm.tmul.congr_simp`
`tmul_tensorAssoc_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticForm` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommGroup` `TensorProduct.leftModule` `CommSemiring.toSemiring` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `TensorProduct.addCommMonoid` `QuadraticMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `tmul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `TensorProduct.assoc` `TensorProduct.smulCommClass_left` `TensorProduct.isScalarTower` `Algebra.toSMul`	—	`Nat.instAtLeastTwoHAddOfNat` `DFunLike.congr_fun` `smulCommClass_self` `TensorProduct.smulCommClass_left` `IsScalarTower.left` `RingHomInvPair.ids` `TensorProduct.isScalarTower` `tmul_comp_tensorAssoc`
`tmul_tensorComm_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticForm` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `CommSemiring.toSemiring` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `QuadraticMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `tmul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `TensorProduct.comm`	—	`Nat.instAtLeastTwoHAddOfNat` `DFunLike.congr_fun` `smulCommClass_self` `IsScalarTower.left` `RingHomInvPair.ids` `tmul_comp_tensorComm`
`tmul_tensorLId_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticForm` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `QuadraticMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `TensorProduct.lid` `Ring.toAddCommGroup` `CommRing.toRing` `TensorProduct.leftModule` `Algebra.to_smulCommClass` `Algebra.id` `tmul` `IsScalarTower.right` `QuadraticMap.sq` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Nat.instAtLeastTwoHAddOfNat` `DFunLike.congr_fun` `Algebra.to_smulCommClass` `RingHomInvPair.ids` `IsScalarTower.right` `comp_tensorLId_eq`
`tmul_tensorMap_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticForm` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `CommSemiring.toSemiring` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `QuadraticMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `tmul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LinearMap` `RingHom.id` `TensorProduct.instModule` `LinearMap.instFunLike` `TensorProduct.map` `QuadraticMap.Isometry.toLinearMap`	—	`Nat.instAtLeastTwoHAddOfNat` `DFunLike.congr_fun` `smulCommClass_self` `IsScalarTower.left` `tmul_comp_tensorMap`
`tmul_tensorRId_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticForm` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `QuadraticMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `TensorProduct.rid` `Ring.toAddCommGroup` `CommRing.toRing` `TensorProduct.leftModule` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `tmul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `QuadraticMap.sq` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.to_smulCommClass` `IsScalarTower.right`	—	`Nat.instAtLeastTwoHAddOfNat` `DFunLike.congr_fun` `smulCommClass_self` `RingHomInvPair.ids` `IsScalarTower.left` `Algebra.to_smulCommClass` `IsScalarTower.right` `comp_tensorRId_eq`

QuadraticMap.Isometry

Definitions

Name	Category	Theorems
`tmul` 📖	CompOp	4 math math: `QuadraticModuleCat.toIsometry_whiskerRight`, `QuadraticModuleCat.toIsometry_tensorHom`, `QuadraticModuleCat.toIsometry_whiskerLeft`, `tmul_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tmul_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticMap.Isometry` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `TensorProduct.leftModule` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Semiring.toModule` `QuadraticForm.tmul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instFunLike` `tmul` `LinearMap` `RingHom.id` `TensorProduct.instModule` `LinearMap.instFunLike` `TensorProduct.map` `toLinearMap`	—	`Nat.instAtLeastTwoHAddOfNat` `smulCommClass_self` `IsScalarTower.left`

---

← Back to Index