Documentation Verification Report

OrzechProperty

📁 Source: Mathlib/LinearAlgebra/Dimension/OrzechProperty.lean

Statistics

Metric	Count
Definitions `basisOfTopLeSpanOfCardEqFinrank`, `finsetBasisOfTopLeSpanOfCardEqFinrank`, `setBasisOfTopLeSpanOfCardEqFinrank`	3
Theorems `coe_basisOfTopLeSpanOfCardEqFinrank`, `finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply`, `linearIndependent_iff_card_eq_finrank_span`, `linearIndependent_iff_card_le_finrank_span`, `linearIndependent_of_top_le_span_of_card_eq_finrank`, `linearIndependent_of_top_le_span_of_card_le_finrank`, `setBasisOfTopLeSpanOfCardEqFinrank_repr_apply`	7
Total	10

(root)

Definitions

Name	Category	Theorems
`basisOfTopLeSpanOfCardEqFinrank` 📖	CompOp	1 math math: `coe_basisOfTopLeSpanOfCardEqFinrank`
`finsetBasisOfTopLeSpanOfCardEqFinrank` 📖	CompOp	1 math math: `finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply`
`setBasisOfTopLeSpanOfCardEqFinrank` 📖	CompOp	1 math math: `setBasisOfTopLeSpanOfCardEqFinrank_repr_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_basisOfTopLeSpanOfCardEqFinrank` 📖	mathematical	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.span` `Set.range` `Fintype.card` `Module.finrank`	`DFunLike.coe` `Module.Basis` `Module.Basis.instFunLike` `basisOfTopLeSpanOfCardEqFinrank`	—	`linearIndependent_of_top_le_span_of_card_eq_finrank`
`finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply` 📖	mathematical	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.span` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.card` `Module.finrank`	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `Finset.instMembership` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `Module.Basis.repr` `finsetBasisOfTopLeSpanOfCardEqFinrank` `LinearMap` `SetLike.instMembership` `Submodule.setLike` `Set.range` `Set` `Set.instMembership` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instFunLike` `LinearIndependent.repr` `linearIndependent_of_top_le_span_of_card_eq_finrank` `Finset.Subtype.fintype` `LinearMap.codRestrict` `LinearMap.id`	—	`RingHomInvPair.ids`
`linearIndependent_iff_card_eq_finrank_span` 📖	mathematical	—	`LinearIndependent` `Fintype.card` `Set.finrank` `Set.range`	—	`finrank_span_eq_card` `strongRankCondition_of_orzechProperty` `Submodule.subset_span` `LinearMap.linearIndependent_iff_of_injOn` `Function.Injective.injOn` `Submodule.subtype_injective` `linearIndependent_of_top_le_span_of_card_eq_finrank` `Function.Injective.mem_set_image` `RingHomSurjective.ids` `Submodule.map_coe` `Submodule.span_image` `Set.range_comp`
`linearIndependent_iff_card_le_finrank_span` 📖	mathematical	—	`LinearIndependent` `Fintype.card` `Set.finrank` `Set.range`	—	`linearIndependent_iff_card_eq_finrank_span` `LE.le.ge_iff_eq'` `finrank_range_le_card` `strongRankCondition_of_orzechProperty`
`linearIndependent_of_top_le_span_of_card_eq_finrank` 📖	mathematical	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.span` `Set.range` `Fintype.card` `Module.finrank`	`LinearIndependent`	—	`linearIndependent_of_top_le_span_of_card_le_finrank` `Eq.le`
`linearIndependent_of_top_le_span_of_card_le_finrank` 📖	mathematical	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.span` `Set.range` `Fintype.card` `Module.finrank`	`LinearIndependent`	—	`Module.Finite.of_surjective` `RingHomSurjective.ids` `Module.Finite.finsupp` `Finite.of_fintype` `Module.Finite.self` `LinearMap.range_eq_top` `top_le_iff` `Finsupp.range_linearCombination` `exists_linearIndependent_of_le_finrank` `OrzechProperty.injective_of_surjective_of_injective` `LinearIndependent.comp` `Equiv.injective`
`setBasisOfTopLeSpanOfCardEqFinrank_repr_apply` 📖	mathematical	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.span` `Finset.card` `Set.toFinset` `Module.finrank`	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `Set.Elem` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `Module.Basis.repr` `setBasisOfTopLeSpanOfCardEqFinrank` `LinearMap` `SetLike.instMembership` `Submodule.setLike` `Set.range` `Set` `Set.instMembership` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instFunLike` `LinearIndependent.repr` `linearIndependent_of_top_le_span_of_card_eq_finrank` `LinearMap.codRestrict` `LinearMap.id`	—	`RingHomInvPair.ids`

---

← Back to Index