Documentation Verification Report

Inversion

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

Statistics

Metric	Count
Definitions `invertibleOfInvertibleι`, `invertibleιOfInvertible`	2
Theorems `invOf_ι`, `invOf_ι_mul_ι_mul_ι`, `isUnit_of_isUnit_ι`, `isUnit_ι_iff`, `isUnit_ι_of_isUnit`, `ι_mul_ι_mul_invOf_ι`	6
Total	8

CliffordAlgebra

Definitions

Name	Category	Theorems
`invertibleOfInvertibleι` 📖	CompOp	—
`invertibleιOfInvertible` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`invOf_ι` 📖	mathematical	—	`Invertible.invOf` `CliffordAlgebra` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `ι` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommRing.toRing` `QuadraticForm` `QuadraticMap.instFunLike` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`Invertible.congr`
`invOf_ι_mul_ι_mul_ι` 📖	mathematical	—	`CliffordAlgebra` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Invertible.invOf` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `ι` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommRing.toRing` `QuadraticForm` `QuadraticMap.instFunLike` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `QuadraticMap.polar` `Ring.toAddCommGroup`	—	`invOf_ι` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `smul_mul_assoc` `IsScalarTower.right` `ι_mul_ι_mul_ι` `smul_sub` `smul_smul` `invOf_mul_self` `one_smul`
`isUnit_of_isUnit_ι` 📖	mathematical	`IsUnit` `CliffordAlgebra` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `instRingCliffordAlgebra` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `ι`	`QuadraticForm` `QuadraticMap.instFunLike` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`Nat.instAtLeastTwoHAddOfNat` `IsUnit.nonempty_invertible` `isUnit_of_invertible`
`isUnit_ι_iff` 📖	mathematical	—	`IsUnit` `CliffordAlgebra` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `instRingCliffordAlgebra` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `ι` `QuadraticForm` `QuadraticMap.instFunLike` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`Nat.instAtLeastTwoHAddOfNat` `isUnit_of_isUnit_ι` `isUnit_ι_of_isUnit`
`isUnit_ι_of_isUnit` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `QuadraticForm` `AddCommGroup.toAddCommMonoid` `QuadraticMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`CliffordAlgebra` `Ring.toSemiring` `instRingCliffordAlgebra` `LinearMap` `RingHom.id` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `ι`	—	`IsUnit.nonempty_invertible` `isUnit_of_invertible`
`ι_mul_ι_mul_invOf_ι` 📖	mathematical	—	`CliffordAlgebra` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `ι` `Invertible.invOf` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommRing.toRing` `QuadraticForm` `QuadraticMap.instFunLike` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `QuadraticMap.polar` `Ring.toAddCommGroup`	—	`invOf_ι` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `mul_smul_comm` `Algebra.to_smulCommClass` `ι_mul_ι_mul_ι` `smul_sub` `smul_smul` `invOf_mul_self` `one_smul`

---

← Back to Index