Documentation Verification Report

Constructions

📁 Source: Mathlib/LinearAlgebra/Projectivization/Constructions.lean

Statistics

Metric	Count
Definitions `cross`, `orthogonal`	2
Theorems `cross_comm`, `cross_mk`, `cross_mk_of_cross_eq_zero`, `cross_mk_of_cross_ne_zero`, `cross_mk_of_ne`, `cross_orthogonal_left`, `cross_orthogonal_right`, `cross_self`, `exists_not_orthogonal_self`, `exists_not_self_orthogonal`, `mk_eq_mk_iff_crossProduct_eq_zero`, `orthogonal_comm`, `orthogonal_cross_left`, `orthogonal_cross_right`, `orthogonal_mk`	15
Total	17

Projectivization

Definitions

Name	Category	Theorems
`cross` 📖	CompOp	10 math math: `cross_orthogonal_left`, `cross_mk_of_cross_ne_zero`, `cross_comm`, `cross_self`, `orthogonal_cross_left`, `cross_orthogonal_right`, `cross_mk`, `orthogonal_cross_right`, `cross_mk_of_ne`, `cross_mk_of_cross_eq_zero`
`orthogonal` 📖	MathDef	9 math math: `cross_orthogonal_left`, `orthogonal_comm`, `exists_not_orthogonal_self`, `exists_not_self_orthogonal`, `orthogonal_cross_left`, `cross_orthogonal_right`, `orthogonal_mk`, `orthogonal_cross_right`, `Configuration.ofField.mem_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cross_comm` 📖	mathematical	—	`cross`	—	`eq_or_ne` `ind` `Function.smulCommClass` `Algebra.to_smulCommClass` `mk_eq_mk_iff_crossProduct_eq_zero` `cross_mk_of_ne` `cross_anticomm` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `cross_self` `neg_zero`
`cross_mk` 📖	mathematical	—	`cross` `Field.toDivisionRing` `Pi.addCommGroup` `Ring.toAddCommGroup` `DivisionRing.toRing` `Pi.Function.module` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `Projectivization` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Function.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Algebra.id` `crossProduct` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Fintype.decidablePiFintype` `Fin.fintype`	—	`Function.smulCommClass` `Algebra.to_smulCommClass`
`cross_mk_of_cross_eq_zero` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Function.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Algebra.id` `crossProduct` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`cross` `Field.toDivisionRing` `Pi.addCommGroup` `Ring.toAddCommGroup` `DivisionRing.toRing` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring`	—	`Function.smulCommClass` `Algebra.to_smulCommClass`
`cross_mk_of_cross_ne_zero` 📖	mathematical	—	`cross` `Field.toDivisionRing` `Pi.addCommGroup` `Ring.toAddCommGroup` `DivisionRing.toRing` `Pi.Function.module` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Function.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Algebra.id` `crossProduct`	—	`Function.smulCommClass` `Algebra.to_smulCommClass`
`cross_mk_of_ne` 📖	mathematical	—	`cross` `Field.toDivisionRing` `Pi.addCommGroup` `Ring.toAddCommGroup` `DivisionRing.toRing` `Pi.Function.module` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Function.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Algebra.id` `crossProduct` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Projectivization` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `mk_eq_mk_iff_crossProduct_eq_zero`	—	`Function.smulCommClass` `Algebra.to_smulCommClass` `mk_eq_mk_iff_crossProduct_eq_zero` `cross_mk_of_cross_ne_zero`
`cross_orthogonal_left` 📖	mathematical	—	`orthogonal` `Fin.fintype` `cross`	—	`ind` `Function.smulCommClass` `Algebra.to_smulCommClass` `mk_eq_mk_iff_crossProduct_eq_zero` `cross_mk_of_ne` `dotProduct_comm` `dot_self_cross`
`cross_orthogonal_right` 📖	mathematical	—	`orthogonal` `Fin.fintype` `cross`	—	`cross_comm` `cross_orthogonal_left`
`cross_self` 📖	mathematical	—	`cross`	—	`ind` `cross_mk_of_cross_eq_zero` `Function.smulCommClass` `Algebra.to_smulCommClass` `mk_eq_mk_iff_crossProduct_eq_zero`
`exists_not_orthogonal_self` 📖	mathematical	—	`orthogonal`	—	`exists_not_self_orthogonal`
`exists_not_self_orthogonal` 📖	mathematical	—	`orthogonal`	—	`ind` `dotProduct_eq_zero_iff` `dotProduct_zero`
`mk_eq_mk_iff_crossProduct_eq_zero` 📖	mathematical	—	`Field.toDivisionRing` `Pi.addCommGroup` `Ring.toAddCommGroup` `DivisionRing.toRing` `Pi.Function.module` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Function.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Algebra.id` `crossProduct` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Function.smulCommClass` `Algebra.to_smulCommClass` `not_iff_not` `mk_eq_mk_iff'` `LinearIndependent.pair_iff'` `crossProduct_ne_zero_iff_linearIndependent` `cross_anticomm` `neg_ne_zero`
`orthogonal_comm` 📖	mathematical	—	`orthogonal`	—	`ind` `dotProduct_comm`
`orthogonal_cross_left` 📖	mathematical	—	`orthogonal` `Fin.fintype` `cross`	—	`orthogonal_comm` `cross_orthogonal_left`
`orthogonal_cross_right` 📖	mathematical	—	`orthogonal` `Fin.fintype` `cross`	—	`orthogonal_comm` `cross_orthogonal_right`
`orthogonal_mk` 📖	mathematical	—	`orthogonal` `Field.toDivisionRing` `Pi.addCommGroup` `Ring.toAddCommGroup` `DivisionRing.toRing` `Pi.Function.module` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—

---

← Back to Index