Documentation Verification Report

ToLinearEquiv

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

Statistics

Metric	Count
Definitions `toLinearEquiv`, `toLinearEquiv'`	2
Theorems `det_ne_zero`, `mul_iff_left`, `mul_iff_right`, `of_det_ne_zero`, `smul_iff`, `det_ne_zero_of_sum_col_pos`, `det_ne_zero_of_sum_row_pos`, `exists_mulVec_eq_zero_iff`, `exists_vecMul_eq_zero_iff`, `ker_toLin_eq_bot`, `nondegenerate_iff_det_ne_zero`, `range_toLin_eq_top`, `separatingLeft_iff_det_ne_zero`, `separatingRight_iff_det_ne_zero`, `toLinearEquiv'_apply`, `toLinearEquiv'_symm_apply`, `toLinearEquiv_apply`	17
Total	19

Matrix

Definitions

Name	Category	Theorems
`toLinearEquiv` 📖	CompOp	1 math math: `toLinearEquiv_apply`
`toLinearEquiv'` 📖	CompOp	4 math math: `toLinearEquiv'_symm_apply`, `toPerfectPairing_apply_apply`, `toLinearEquiv'_apply`, `toPerfectPairing`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`det_ne_zero_of_sum_col_pos` 📖	—	`Pairwise` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.univ`	—	—	`isEmpty_or_nonempty` `coe_det_isEmpty` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Mathlib.Tactic.Contrapose.contrapose₃` `Mathlib.Tactic.Push.not_forall_eq` `exists_vecMul_eq_zero_iff` `IsStrictOrderedRing.isDomain` `AddGroup.existsAddOfLE` `Finset.univ_nonempty` `Finset.exists_mem_eq_sup'` `mul_le_mul_iff_right₀` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Finset.mul_sum` `MulZeroClass.mul_zero` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `le_refl` `mul_le_mul_right_of_neg` `IsStrictOrderedRing.toMulPosStrictMono` `covariant_swap_add_of_covariant_add` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Finset.le_sup'` `neg_smul` `one_smul` `smul_vecMul` `IsScalarTower.right` `smul_zero` `Function.ne_iff` `Pi.smul_apply` `Left.neg_pos_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Ne.lt_of_le`
`det_ne_zero_of_sum_row_pos` 📖	—	`Pairwise` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.univ`	—	—	`det_transpose` `det_ne_zero_of_sum_col_pos` `Finset.sum_congr`
`exists_mulVec_eq_zero_iff` 📖	mathematical	—	`mulVec` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `det`	—	`IsDomain.toNontrivial` `Localization.isLocalization`
`exists_vecMul_eq_zero_iff` 📖	mathematical	—	`vecMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `det`	—	`det_transpose` `exists_mulVec_eq_zero_iff`
`ker_toLin_eq_bot` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `det`	`LinearMap.ker` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `DFunLike.coe` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `LinearMap` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.addCommMonoid` `module` `Semiring.toModule` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLin` `Finite.of_fintype` `Bot.bot` `Submodule` `Submodule.instBot`	—	`RingHomInvPair.ids` `smulCommClass_self` `Finite.of_fintype` `LinearMap.ker_eq_bot` `LinearEquiv.injective`
`nondegenerate_iff_det_ne_zero` 📖	mathematical	—	`Nondegenerate` `Finite.of_fintype`	—	`Finite.of_fintype` `exists_vecMul_eq_zero_iff` `Mathlib.Tactic.Push.not_and_eq` `Nondegenerate.exists_not_ortho_of_ne_zero` `dotProduct_mulVec` `zero_dotProduct` `nondegenerate_of_det_ne_zero`
`range_toLin_eq_top` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `det`	`LinearMap.range` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `DFunLike.coe` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `LinearMap` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.addCommMonoid` `module` `Semiring.toModule` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLin` `Finite.of_fintype` `Top.top` `Submodule` `Submodule.instTop`	—	`RingHomSurjective.ids` `RingHomInvPair.ids` `smulCommClass_self` `Finite.of_fintype` `LinearMap.range_eq_top` `LinearEquiv.surjective`
`separatingLeft_iff_det_ne_zero` 📖	mathematical	—	`SeparatingLeft` `Finite.of_fintype`	—	`Finite.of_fintype` `exists_vecMul_eq_zero_iff` `separatingLeft_def` `dotProduct_mulVec` `zero_dotProduct` `Nondegenerate.separatingLeft` `nondegenerate_of_det_ne_zero`
`separatingRight_iff_det_ne_zero` 📖	mathematical	—	`SeparatingRight` `Finite.of_fintype`	—	`Finite.of_fintype` `exists_mulVec_eq_zero_iff` `separatingRight_def` `dotProduct_zero` `Nondegenerate.separatingRight` `nondegenerate_of_det_ne_zero`
`toLinearEquiv'_apply` 📖	mathematical	—	`LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `toLinearEquiv'` `DFunLike.coe` `LinearEquiv` `Matrix` `LinearMap` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `addCommMonoid` `LinearMap.addCommMonoid` `module` `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` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLin'`	—	`RingHomInvPair.ids`
`toLinearEquiv'_symm_apply` 📖	mathematical	—	`LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `LinearEquiv.symm` `toLinearEquiv'` `DFunLike.coe` `LinearEquiv` `Matrix` `LinearMap` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `addCommMonoid` `LinearMap.addCommMonoid` `module` `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` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLin'` `Invertible.invOf` `instMulOfFintypeOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`RingHomInvPair.ids`
`toLinearEquiv_apply` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `det`	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `toLinearEquiv` `LinearMap` `LinearMap.instFunLike` `Matrix` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.addCommMonoid` `module` `Semiring.toModule` `LinearMap.module` `DFinsupp.instEquivLikeLinearEquiv` `toLin` `Finite.of_fintype`	—	`RingHomInvPair.ids`

Matrix.Nondegenerate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`det_ne_zero` 📖	—	`Matrix.Nondegenerate` `Finite.of_fintype`	—	—	`Finite.of_fintype` `Matrix.nondegenerate_iff_det_ne_zero`
`mul_iff_left` 📖	mathematical	`Matrix.Nondegenerate` `Finite.of_fintype`	`Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`Finite.of_fintype` `Matrix.det_mul` `mul_ne_zero_iff_left` `IsDomain.to_noZeroDivisors`
`mul_iff_right` 📖	mathematical	`Matrix.Nondegenerate` `Finite.of_fintype`	`Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`Finite.of_fintype` `Matrix.det_mul` `mul_ne_zero_iff_right` `IsDomain.to_noZeroDivisors`
`of_det_ne_zero` 📖	mathematical	—	`Matrix.Nondegenerate` `Finite.of_fintype`	—	`Finite.of_fintype` `Matrix.nondegenerate_iff_det_ne_zero`
`smul_iff` 📖	mathematical	—	`Matrix.Nondegenerate` `Matrix` `Matrix.smul` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	—	`Finite.of_fintype` `Matrix.nondegenerate_def` `Matrix.smul_mulVec` `IsScalarTower.right` `dotProduct_smul` `Algebra.to_smulCommClass` `mul_eq_zero_iff_left` `IsDomain.to_noZeroDivisors`

---

← Back to Index