Documentation Verification Report

Matrix

📁 Source: Mathlib/LinearAlgebra/AffineSpace/Matrix.lean

Statistics

Metric	Count
Definitions `toMatrix`	1
Theorems `affineIndependent_of_toMatrix_right_inv`, `affineSpan_eq_top_of_toMatrix_left_inv`, `det_smul_coords_eq_cramer_coords`, `isUnit_toMatrix`, `isUnit_toMatrix_iff`, `toMatrix_apply`, `toMatrix_inv_vecMul_toMatrix`, `toMatrix_mul_toMatrix`, `toMatrix_row_sum_one`, `toMatrix_self`, `toMatrix_vecMul_coords`	11
Total	12

AffineBasis

Definitions

Name	Category	Theorems
`toMatrix` 📖	CompOp	9 math math: `toMatrix_mul_toMatrix`, `toMatrix_apply`, `toMatrix_vecMul_coords`, `det_smul_coords_eq_cramer_coords`, `toMatrix_inv_vecMul_toMatrix`, `toMatrix_row_sum_one`, `isUnit_toMatrix_iff`, `toMatrix_self`, `isUnit_toMatrix`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affineIndependent_of_toMatrix_right_inv` 📖	mathematical	`Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `toMatrix` `Matrix.one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`AffineIndependent`	—	`nonempty_fintype` `affineIndependent_iff_eq_of_fintype_affineCombination_eq` `Finset.affineCombination_eq_linear_combination` `Finset.map_affineCombination` `Matrix.vecMul_vecMul` `Matrix.vecMul_one`
`affineSpan_eq_top_of_toMatrix_left_inv` 📖	mathematical	`Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `toMatrix` `Matrix.one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`affineSpan` `Set.range` `Top.top` `AffineSubspace` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `AffineSubspace.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`nonempty_fintype` `Finset.sum_congr` `sum_coord_apply_eq_one` `mul_one` `Finset.mul_sum` `Finset.sum_comm` `Finset.sum_ite_eq` `ext_elem` `coord_apply` `Finset.map_affineCombination` `Finset.affineCombination_eq_linear_combination` `affineCombination_mem_affineSpan` `eq_top_iff` `tot` `affineSpan_le`
`det_smul_coords_eq_cramer_coords` 📖	mathematical	—	`Function.hasSMul` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Matrix.det` `toMatrix` `CommRing.toRing` `DFunLike.coe` `AffineBasis` `instFunLike` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `coords` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearMap.instFunLike` `Matrix.cramer` `Matrix.transpose`	—	`isUnit_toMatrix` `toMatrix_inv_vecMul_toMatrix` `Matrix.det_smul_inv_vecMul_eq_cramer_transpose` `Matrix.isUnit_iff_isUnit_det`
`isUnit_toMatrix` 📖	mathematical	—	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Ring.toSemiring` `toMatrix` `DFunLike.coe` `AffineBasis` `instFunLike`	—	`toMatrix_mul_toMatrix`
`isUnit_toMatrix_iff` 📖	mathematical	—	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Ring.toSemiring` `toMatrix` `AffineIndependent` `affineSpan` `Set.range` `Top.top` `AffineSubspace` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `AffineSubspace.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`affineIndependent_of_toMatrix_right_inv` `Finite.of_fintype` `affineSpan_eq_top_of_toMatrix_left_inv` `isUnit_toMatrix`
`toMatrix_apply` 📖	mathematical	—	`toMatrix` `DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `coord`	—	—
`toMatrix_inv_vecMul_toMatrix` 📖	mathematical	—	`Matrix.vecMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `AffineMap` `CommRing.toRing` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `coords` `Matrix` `Matrix.inv` `toMatrix` `AffineBasis` `instFunLike`	—	`isUnit_toMatrix` `toMatrix_vecMul_coords` `Matrix.vecMul_vecMul` `Matrix.mul_nonsing_inv` `Matrix.isUnit_iff_isUnit_det` `Matrix.vecMul_one`
`toMatrix_mul_toMatrix` 📖	mathematical	—	`Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `toMatrix` `DFunLike.coe` `AffineBasis` `instFunLike` `Matrix.one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Matrix.ext` `toMatrix_vecMul_coords` `coords_apply` `toMatrix_apply` `toMatrix_self`
`toMatrix_row_sum_one` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.univ` `toMatrix` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Finset.sum_congr` `sum_coord_apply_eq_one`
`toMatrix_self` 📖	mathematical	—	`toMatrix` `DFunLike.coe` `AffineBasis` `instFunLike` `Matrix` `Matrix.one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Matrix.ext` `toMatrix_apply` `coord_apply` `Matrix.one_eq_pi_single` `Pi.single_apply`
`toMatrix_vecMul_coords` 📖	mathematical	—	`Matrix.vecMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `coords` `toMatrix` `AffineBasis` `instFunLike`	—	`affineCombination_coord_eq_self` `Finset.map_affineCombination` `sum_coord_apply_eq_one` `Finset.sum_congr` `Finset.affineCombination_eq_linear_combination`

---

← Back to Index