Documentation Verification Report

Projective

📁 Source: Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Projective.lean

Statistics

Metric	Count
Definitions `ProjGenLinGroup`, `mk`, `mulActionOfGL`, `signDet`, `instGroupProjGenLinGroup`, `«termPGL(_,_)_1»`_1»), `«termPGL(_,_)»`»)	7
Theorems `induction_on`, `ker_mk`, `lift_comp_mk`, `lift_mk`, `mk_scalar`, `mk_smul`, `mk_surjective`, `signDet_mk`, `val_signDet_mk`	9
Total	16

Matrix

Definitions

Name	Category	Theorems
`ProjGenLinGroup` 📖	CompOp	8 math math: `ProjGenLinGroup.mk_scalar`, `ProjGenLinGroup.lift_mk`, `ProjGenLinGroup.ker_mk`, `ProjGenLinGroup.mk_surjective`, `ProjGenLinGroup.val_signDet_mk`, `ProjGenLinGroup.signDet_mk`, `ProjGenLinGroup.lift_comp_mk`, `ProjGenLinGroup.mk_smul`
`instGroupProjGenLinGroup` 📖	CompOp	8 math math: `ProjGenLinGroup.mk_scalar`, `ProjGenLinGroup.lift_mk`, `ProjGenLinGroup.ker_mk`, `ProjGenLinGroup.mk_surjective`, `ProjGenLinGroup.val_signDet_mk`, `ProjGenLinGroup.signDet_mk`, `ProjGenLinGroup.lift_comp_mk`, `ProjGenLinGroup.mk_smul`

Matrix.ProjGenLinGroup

Definitions

Name	Category	Theorems
`mk` 📖	CompOp	—
`mulActionOfGL` 📖	CompOp	1 math math: `mk_smul`
`signDet` 📖	CompOp	2 math math: `val_signDet_mk`, `signDet_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`induction_on` 📖	—	`DFunLike.coe` `MonoidHom` `Matrix.GeneralLinearGroup` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Matrix.ProjGenLinGroup` `MulOneClass.toMulOne` `Units.instMulOneClass` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Matrix.instGroupProjGenLinGroup` `MonoidHom.instFunLike`	—	—	—
`ker_mk` 📖	mathematical	—	`MonoidHom.ker` `Matrix.GeneralLinearGroup` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Matrix.ProjGenLinGroup` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Matrix.instGroupProjGenLinGroup` `Subgroup.center`	—	`QuotientGroup.ker_mk'`
`lift_comp_mk` 📖	mathematical	`MonoidHom.comp` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Matrix.GeneralLinearGroup` `MulOneClass.toMulOne` `Units.instMulOneClass` `Matrix` `Matrix.semiring` `Monoid.toMulOneClass` `Matrix.GeneralLinearGroup.scalar` `MonoidHom` `instOneMonoidHom`	`MonoidHom.comp` `Matrix.GeneralLinearGroup` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Matrix.ProjGenLinGroup` `MulOneClass.toMulOne` `Units.instMulOneClass` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Matrix.instGroupProjGenLinGroup` `lift`	—	—
`lift_mk` 📖	mathematical	`MonoidHom.comp` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Matrix.GeneralLinearGroup` `MulOneClass.toMulOne` `Units.instMulOneClass` `Matrix` `Matrix.semiring` `Monoid.toMulOneClass` `Matrix.GeneralLinearGroup.scalar` `MonoidHom` `instOneMonoidHom`	`DFunLike.coe` `MonoidHom` `Matrix.ProjGenLinGroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Matrix.instGroupProjGenLinGroup` `MonoidHom.instFunLike` `lift` `Matrix.GeneralLinearGroup` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Units.instMulOneClass` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring`	—	—
`mk_scalar` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Matrix.GeneralLinearGroup` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Matrix.ProjGenLinGroup` `MulOneClass.toMulOne` `Units.instMulOneClass` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Matrix.instGroupProjGenLinGroup` `MonoidHom.instFunLike` `Units` `Matrix.GeneralLinearGroup.scalar` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`MonoidHom.mem_ker` `Matrix.GeneralLinearGroup.center_eq_range_scalar`
`mk_smul` 📖	mathematical	`Matrix.GeneralLinearGroup` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Units.instMonoid` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `MulAction.toSemigroupAction` `DFunLike.coe` `MonoidHom` `Units` `MulOneClass.toMulOne` `Units.instMulOneClass` `MonoidHom.instFunLike` `Matrix.GeneralLinearGroup.scalar`	`Matrix.ProjGenLinGroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Matrix.instGroupProjGenLinGroup` `MulAction.toSemigroupAction` `mulActionOfGL` `DFunLike.coe` `MonoidHom` `Matrix.GeneralLinearGroup` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MulOneClass.toMulOne` `Units.instMulOneClass` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Units.instMonoid`	—	—
`mk_surjective` 📖	mathematical	—	`Matrix.GeneralLinearGroup` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Matrix.ProjGenLinGroup` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Units.instMulOneClass` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Matrix.instGroupProjGenLinGroup` `MonoidHom.instFunLike`	—	`Quotient.mk_surjective`
`signDet_mk` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Matrix.ProjGenLinGroup` `Units` `SignType` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `SignType.instCommGroupWithZero` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Matrix.instGroupProjGenLinGroup` `Units.instMulOneClass` `MonoidHom.instFunLike` `signDet` `Matrix.GeneralLinearGroup` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Matrix` `Semiring.toMonoidWithZero` `Matrix.semiring` `Units.map` `MonoidWithZeroHom.toMonoidHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `MonoidWithZero.toMulZeroOneClass` `signHom` `Matrix.GeneralLinearGroup.det`	—	—
`val_signDet_mk` 📖	mathematical	—	`Units.val` `SignType` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `SignType.instCommGroupWithZero` `DFunLike.coe` `MonoidHom` `Matrix.ProjGenLinGroup` `Units` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Matrix.instGroupProjGenLinGroup` `Units.instMulOneClass` `MonoidHom.instFunLike` `signDet` `Matrix.GeneralLinearGroup` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Matrix` `Semiring.toMonoidWithZero` `Matrix.semiring` `OrderHom` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearOrder.toDecidableLT` `Matrix.GeneralLinearGroup.det`	—	—

MatrixGroups

Definitions

Name	Category	Theorems
`«termPGL(_,_)_1»` 📖_1» "API Documentation")	CompOp	—
`«termPGL(_,_)»` 📖» "API Documentation")	CompOp	—

---

← Back to Index