Documentation Verification Report

Prod

📁 Source: Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean

Statistics

Metric	Count
Definitions `ofProd`, `prodEquiv`, `toProd`	3
Theorems `commute_map_mul_map_of_isOrtho_of_mem_evenOdd_zero_left`, `commute_map_mul_map_of_isOrtho_of_mem_evenOdd_zero_right`, `map_mul_map_eq_neg_of_isOrtho_of_mem_evenOdd_one`, `map_mul_map_of_isOrtho_of_mem_evenOdd`, `ofProd_comp_toProd`, `ofProd_ι_mk`, `prodEquiv_apply`, `prodEquiv_symm_apply`, `toProd_comp_ofProd`, `toProd_one_tmul_ι`, `toProd_ι_tmul_one`	11
Total	14

CliffordAlgebra

Definitions

Name	Category	Theorems
`ofProd` 📖	CompOp	4 math math: `toProd_comp_ofProd`, `prodEquiv_apply`, `ofProd_comp_toProd`, `ofProd_ι_mk`
`prodEquiv` 📖	CompOp	2 math math: `prodEquiv_symm_apply`, `prodEquiv_apply`
`toProd` 📖	CompOp	5 math math: `toProd_comp_ofProd`, `toProd_ι_tmul_one`, `prodEquiv_symm_apply`, `ofProd_comp_toProd`, `toProd_one_tmul_ι`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commute_map_mul_map_of_isOrtho_of_mem_evenOdd_zero_left` 📖	mathematical	`QuadraticMap.IsOrtho` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `DFunLike.coe` `QuadraticMap.Isometry` `QuadraticMap.Isometry.instFunLike` `CliffordAlgebra` `Submodule` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `SetLike.instMembership` `Submodule.setLike` `evenOdd` `ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing`	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AlgHom` `AlgHom.funLike` `map`	—	`map_mul_map_of_isOrtho_of_mem_evenOdd` `MulZeroClass.mul_zero` `uzpow_zero` `one_smul`
`commute_map_mul_map_of_isOrtho_of_mem_evenOdd_zero_right` 📖	mathematical	`QuadraticMap.IsOrtho` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `DFunLike.coe` `QuadraticMap.Isometry` `QuadraticMap.Isometry.instFunLike` `CliffordAlgebra` `Submodule` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `SetLike.instMembership` `Submodule.setLike` `evenOdd` `ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing`	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AlgHom` `AlgHom.funLike` `map`	—	`map_mul_map_of_isOrtho_of_mem_evenOdd` `MulZeroClass.zero_mul` `uzpow_zero` `one_smul`
`map_mul_map_eq_neg_of_isOrtho_of_mem_evenOdd_one` 📖	mathematical	`QuadraticMap.IsOrtho` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `DFunLike.coe` `QuadraticMap.Isometry` `QuadraticMap.Isometry.instFunLike` `CliffordAlgebra` `Submodule` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `SetLike.instMembership` `Submodule.setLike` `evenOdd` `ZMod` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AlgHom` `AlgHom.funLike` `map` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`map_mul_map_of_isOrtho_of_mem_evenOdd` `mul_one` `uzpow_one` `Units.neg_smul` `one_smul` `neg_mul`
`map_mul_map_of_isOrtho_of_mem_evenOdd` 📖	mathematical	`QuadraticMap.IsOrtho` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `DFunLike.coe` `QuadraticMap.Isometry` `QuadraticMap.Isometry.instFunLike` `CliffordAlgebra` `Submodule` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `SetLike.instMembership` `Submodule.setLike` `evenOdd`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AlgHom` `AlgHom.funLike` `map` `Units` `Int.instMonoid` `Units.instSMul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `ZMod` `Int.instUnitsPow` `ZMod.commRing` `instModuleZModOfNatNatAdditiveUnitsInt` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `Units.instOne`	—	`Submodule.iSup_induction'` `Submodule.pow_induction_on_left'` `AlgHom.commutes` `Nat.cast_zero` `MulZeroClass.mul_zero` `uzpow_zero` `one_smul` `Algebra.commutes` `IsScalarTower.right` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `add_mul` `Distrib.rightDistribClass` `mul_add` `Distrib.leftDistribClass` `smul_add` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `mul_assoc` `mul_smul_comm` `Units.smulCommClass_left` `Algebra.to_smulCommClass` `AddCommGroup.intIsScalarTower` `map_apply_ι` `Nat.cast_succ` `mul_add_one` `uzpow_add` `SemigroupAction.mul_smul` `smul_mul_assoc` `Units.instIsScalarTower` `ι_mul_ι_comm_of_isOrtho` `neg_mul` `Units.neg_smul` `uzpow_one` `mul_neg_one` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `MulZeroClass.zero_mul` `smul_zero`
`ofProd_comp_toProd` 📖	mathematical	—	`AlgHom.comp` `GradedTensorProduct` `ZMod` `CliffordAlgebra` `CommRing.toCommSemiring` `ZMod.commRing` `ZMod.decidableEq` `instRingCliffordAlgebra` `instAlgebraCliffordAlgebra` `evenOdd` `gradedAlgebra` `Prod.instAddCommGroup` `Prod.instModule` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `QuadraticMap.prod` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ring.toSemiring` `GradedTensorProduct.instRing` `instModuleZModOfNatNatAdditiveUnitsInt` `GradedTensorProduct.instAlgebra` `ofProd` `toProd` `AlgHom.id`	—	`GradedTensorProduct.algHom_ext` `hom_ext` `LinearMap.ext` `RingHomCompTriple.ids` `toProd_ι_tmul_one` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `EquivLike.toEmbeddingLike` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `TensorProduct.tmul_zero` `toProd_one_tmul_ι` `AddRightCancelSemigroup.toIsRightCancelAdd` `TensorProduct.zero_tmul`
`ofProd_ι_mk` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `CliffordAlgebra` `Prod.instAddCommGroup` `Prod.instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `QuadraticMap.prod` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `GradedTensorProduct` `ZMod` `ZMod.commRing` `ZMod.decidableEq` `instRingCliffordAlgebra` `instAlgebraCliffordAlgebra` `evenOdd` `gradedAlgebra` `Ring.toSemiring` `GradedTensorProduct.instRing` `instModuleZModOfNatNatAdditiveUnitsInt` `GradedTensorProduct.instAlgebra` `AlgHom.funLike` `ofProd` `LinearMap` `RingHom.id` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `LinearMap.instFunLike` `ι` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `GradedTensorProduct.tmul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`ι_mem_evenOdd_one` `ofProd.eq_1` `lift_ι_apply`
`prodEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `CliffordAlgebra` `Prod.instAddCommGroup` `Prod.instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `QuadraticMap.prod` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `GradedTensorProduct` `ZMod` `ZMod.commRing` `ZMod.decidableEq` `instRingCliffordAlgebra` `instAlgebraCliffordAlgebra` `evenOdd` `gradedAlgebra` `Ring.toSemiring` `GradedTensorProduct.instRing` `instModuleZModOfNatNatAdditiveUnitsInt` `GradedTensorProduct.instAlgebra` `AlgEquiv.instFunLike` `prodEquiv` `AlgHom` `AlgHom.funLike` `ofProd`	—	—
`prodEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `GradedTensorProduct` `ZMod` `CliffordAlgebra` `CommRing.toCommSemiring` `ZMod.commRing` `ZMod.decidableEq` `instRingCliffordAlgebra` `instAlgebraCliffordAlgebra` `evenOdd` `gradedAlgebra` `Prod.instAddCommGroup` `Prod.instModule` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `QuadraticMap.prod` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ring.toSemiring` `GradedTensorProduct.instRing` `instModuleZModOfNatNatAdditiveUnitsInt` `GradedTensorProduct.instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `prodEquiv` `AlgHom` `AlgHom.funLike` `toProd`	—	—
`toProd_comp_ofProd` 📖	mathematical	—	`AlgHom.comp` `CliffordAlgebra` `Prod.instAddCommGroup` `Prod.instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `QuadraticMap.prod` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `GradedTensorProduct` `ZMod` `ZMod.commRing` `ZMod.decidableEq` `instRingCliffordAlgebra` `instAlgebraCliffordAlgebra` `evenOdd` `gradedAlgebra` `Ring.toSemiring` `GradedTensorProduct.instRing` `instModuleZModOfNatNatAdditiveUnitsInt` `GradedTensorProduct.instAlgebra` `toProd` `ofProd` `AlgHom.id`	—	`hom_ext` `LinearMap.prod_ext` `RingHomCompTriple.ids` `LinearMap.ext` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `toProd_one_tmul_ι` `toProd_ι_tmul_one` `Prod.mk_zero_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `add_zero` `zero_add`
`toProd_one_tmul_ι` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `GradedTensorProduct` `ZMod` `CliffordAlgebra` `CommRing.toCommSemiring` `ZMod.commRing` `ZMod.decidableEq` `instRingCliffordAlgebra` `instAlgebraCliffordAlgebra` `evenOdd` `gradedAlgebra` `Prod.instAddCommGroup` `Prod.instModule` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `QuadraticMap.prod` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ring.toSemiring` `GradedTensorProduct.instRing` `instModuleZModOfNatNatAdditiveUnitsInt` `GradedTensorProduct.instAlgebra` `AlgHom.funLike` `toProd` `GradedTensorProduct.tmul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `LinearMap` `RingHom.id` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `LinearMap.instFunLike` `ι` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`toProd.eq_1` `GradedTensorProduct.lift_tmul` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `one_mul` `map_apply_ι` `QuadraticMap.Isometry.inr_apply`
`toProd_ι_tmul_one` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `GradedTensorProduct` `ZMod` `CliffordAlgebra` `CommRing.toCommSemiring` `ZMod.commRing` `ZMod.decidableEq` `instRingCliffordAlgebra` `instAlgebraCliffordAlgebra` `evenOdd` `gradedAlgebra` `Prod.instAddCommGroup` `Prod.instModule` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `QuadraticMap.prod` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ring.toSemiring` `GradedTensorProduct.instRing` `instModuleZModOfNatNatAdditiveUnitsInt` `GradedTensorProduct.instAlgebra` `AlgHom.funLike` `toProd` `GradedTensorProduct.tmul` `LinearMap` `RingHom.id` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `LinearMap.instFunLike` `ι` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`toProd.eq_1` `GradedTensorProduct.lift_tmul` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `mul_one` `map_apply_ι` `QuadraticMap.Isometry.inl_apply`

---

← Back to Index