Documentation Verification Report

RankNullity

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

Statistics

Metric	Count
Definitions `HasRankNullity`	1
Theorems `exists_set_linearIndependent`, `rank_quotient_add_rank`, `lift_rank_eq_of_surjective`, `lift_rank_range_add_rank_ker`, `rank_eq_of_surjective`, `rank_range_add_rank_ker`, `disjoint_ker_of_finrank_le`, `exists_of_finrank_lt`, `exists_smul_notMem_of_rank_lt`, `finrank_quotient`, `finrank_quotient_add_finrank`, `rank_add_le_rank_add_rank`, `rank_quotient_add_rank`, `rank_sup_add_rank_inf_eq`, `exists_linearIndepOn_of_lt_rank`, `exists_linearIndependent_cons_of_lt_finrank`, `exists_linearIndependent_cons_of_lt_rank`, `exists_linearIndependent_pair_of_one_lt_finrank`, `exists_linearIndependent_pair_of_one_lt_rank`, `exists_linearIndependent_snoc_of_lt_finrank`, `exists_linearIndependent_snoc_of_lt_rank`, `exists_set_linearIndependent`, `nontrivial_of_hasRankNullity`	23
Total	24

HasRankNullity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_set_linearIndependent` 📖	mathematical	—	`Set.Elem` `Module.rank` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearIndepOn`	—	—
`rank_quotient_add_rank` 📖	mathematical	—	`Cardinal` `Cardinal.instAdd` `Module.rank` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	—

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lift_rank_eq_of_surjective` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike`	`Cardinal.lift` `Module.rank` `Cardinal` `Cardinal.instAdd` `Submodule` `SetLike.instMembership` `Submodule.setLike` `ker` `Submodule.addCommMonoid` `Submodule.module`	—	`RingHomSurjective.ids` `lift_rank_range_add_rank_ker` `rank_range_of_surjective`
`lift_rank_range_add_rank_ker` 📖	mathematical	—	`Cardinal` `Cardinal.instAdd` `Cardinal.lift` `Module.rank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.addCommMonoid` `Submodule.module` `ker`	—	`RingHomSurjective.ids` `LinearEquiv.lift_rank_eq` `Cardinal.lift_add` `Submodule.rank_quotient_add_rank`
`rank_eq_of_surjective` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike`	`Module.rank` `Cardinal` `Cardinal.instAdd` `Submodule` `SetLike.instMembership` `Submodule.setLike` `ker` `Submodule.addCommMonoid` `Submodule.module`	—	`RingHomSurjective.ids` `rank_range_add_rank_ker` `rank_range_of_surjective`
`rank_range_add_rank_ker` 📖	mathematical	—	`Cardinal` `Cardinal.instAdd` `Module.rank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.addCommMonoid` `Submodule.module` `ker`	—	`RingHomSurjective.ids` `LinearEquiv.rank_eq` `Submodule.rank_quotient_add_rank`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_ker_of_finrank_le` 📖	mathematical	`Module.finrank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `map` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids`	`Disjoint` `instPartialOrder` `instOrderBot` `LinearMap.ker`	—	`RingHomSurjective.ids` `disjoint_iff` `LinearMap.injective_domRestrict_iff` `LinearMap.ker_eq_bot` `rank_eq_zero` `Ideal.instIsTorsionFreeSubtypeMemSubmodule` `finrank_eq_rank` `Nat.cast_eq_zero` `Cardinal.instCharZero` `finrank_quotient_add_finrank` `LinearMap.range_domRestrict` `LinearEquiv.finrank_eq`
`exists_of_finrank_lt` 📖	mathematical	`Module.finrank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`exists_finset_linearIndependent_of_le_finrank` `le_rfl` `Finset.nonempty_iff_ne_empty` `Finset.card_eq_zero` `finrank_quotient` `tsub_eq_zero_iff_le` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `not_le` `mkQ_surjective` `linearIndependent_iff` `Quotient.mk_eq_zero` `mkQ_apply` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finsupp.single_eq_zero` `Finsupp.linearCombination_single`
`exists_smul_notMem_of_rank_lt` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Module.rank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`LT.lt.ne` `zero_add` `rank_quotient_add_rank` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Mathlib.Tactic.Push.not_forall_eq` `Mathlib.Tactic.Push.not_and_eq` `Function.Surjective.forall` `Quotient.mk_surjective` `rank_eq_zero_iff`
`finrank_quotient` 📖	mathematical	—	`Module.finrank` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `hasQuotient` `Quotient.addCommGroup` `Quotient.module'` `SetLike.instMembership` `setLike` `addCommMonoid` `module'`	—	`finrank_quotient_add_finrank`
`finrank_quotient_add_finrank` 📖	mathematical	—	`Module.finrank` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `hasQuotient` `Quotient.addCommGroup` `Quotient.module` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	—	`Cardinal.instCharZero` `Module.finrank_eq_rank` `Nat.cast_add` `Module.Finite.quotient` `finrank_eq_rank` `HasRankNullity.rank_quotient_add_rank`
`rank_add_le_rank_add_rank` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Module.rank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `addCommMonoid` `module` `Cardinal.instAdd`	—	`rank_sup_add_rank_inf_eq` `self_le_add_right` `Cardinal.canonicallyOrderedAdd`
`rank_quotient_add_rank` 📖	mathematical	—	`Cardinal` `Cardinal.instAdd` `Module.rank` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `hasQuotient` `Quotient.addCommGroup` `Quotient.module` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	—	`HasRankNullity.rank_quotient_add_rank`
`rank_sup_add_rank_inf_eq` 📖	mathematical	—	`Cardinal` `Cardinal.instAdd` `Module.rank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `addCommMonoid` `module` `instMin`	—	`inf_of_le_right` `rank_quotient_add_rank` `comap_inf` `LinearEquiv.rank_eq` `RingHomSurjective.ids` `map_comap_subtype` `inf_assoc` `inf_idem` `add_right_comm`

(root)

Definitions

Name	Category	Theorems
`HasRankNullity` 📖	CompData	2 math math: `IsDomain.hasRankNullity`, `DivisionRing.hasRankNullity`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_linearIndepOn_of_lt_rank` 📖	mathematical	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	`Set` `Set.instHasSubset` `Set.Elem` `Module.rank`	—	`exists_set_linearIndependent` `Set.disjoint_iff` `LinearIndependent.ne_zero` `nontrivial_of_hasRankNullity` `Submodule.mkQ_apply` `Submodule.Quotient.mk_eq_zero` `Submodule.subset_span` `Set.subset_union_left` `Cardinal.mk_union_of_disjoint` `Cardinal.mk_image_eq` `Submodule.rank_quotient_add_rank` `add_comm` `rank_span_set` `LinearIndepOn.union_id_of_quotient` `linearIndepOn_iff_image` `Set.InjOn.image_of_comp` `Function.Injective.injOn` `Set.image_comp` `Set.image_id` `Submodule.mkQ_surjective`
`exists_linearIndependent_cons_of_lt_finrank` 📖	mathematical	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Module.finrank`	`Fin.cons`	—	`exists_linearIndependent_cons_of_lt_rank` `Module.lt_rank_of_lt_finrank`
`exists_linearIndependent_cons_of_lt_rank` 📖	mathematical	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Cardinal.instNatCast` `Module.rank`	`Fin.cons`	—	`exists_linearIndepOn_of_lt_rank` `LinearIndependent.linearIndepOn_id` `LT.lt.ne` `Cardinal.mk_fintype` `Fintype.card_fin` `Cardinal.lift_natCast` `Cardinal.lift_id'` `Cardinal.mk_range_eq_of_injective` `LinearIndependent.injective` `nontrivial_of_hasRankNullity` `Cardinal.lift_injective` `Set.nonempty_of_ssubset` `HasSubset.Subset.ssubset_of_ne` `Set.instIsNonstrictStrictOrderSubsetSSubset` `Set.instAntisymmSubset` `linearIndepOn_id_range_iff` `Fin.cons_injective_iff` `LinearIndepOn.mono` `Set.insert_subset` `Fin.range_cons`
`exists_linearIndependent_pair_of_one_lt_finrank` 📖	mathematical	`Module.finrank` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	`LinearIndependent` `Matrix.vecCons` `Matrix.vecEmpty`	—	`exists_linearIndependent_pair_of_one_lt_rank` `Module.one_lt_rank_of_one_lt_finrank`
`exists_linearIndependent_pair_of_one_lt_rank` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Cardinal.instOne` `Module.rank` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	`LinearIndependent` `Matrix.vecCons` `Matrix.vecEmpty`	—	`exists_linearIndependent_snoc_of_lt_rank` `LinearIndependent.of_subsingleton` `Nat.instZeroLEOneClass` `Matrix.cons_val_fin_one` `zero_add` `Matrix.cons_val_succ`
`exists_linearIndependent_snoc_of_lt_finrank` 📖	mathematical	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Module.finrank`	`Fin.snoc`	—	`exists_linearIndependent_snoc_of_lt_rank` `Module.lt_rank_of_lt_finrank`
`exists_linearIndependent_snoc_of_lt_rank` 📖	mathematical	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Cardinal.instNatCast` `Module.rank`	`Fin.snoc`	—	`Fin.snoc_eq_cons_rotate` `exists_linearIndependent_cons_of_lt_rank` `LinearIndependent.comp` `Equiv.injective`
`exists_set_linearIndependent` 📖	mathematical	—	`Set.Elem` `Module.rank` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearIndependent` `Set` `Set.instMembership`	—	`HasRankNullity.exists_set_linearIndependent`
`nontrivial_of_hasRankNullity` 📖	mathematical	—	`Nontrivial`	—	`subsingleton_or_nontrivial` `Submodule.rank_quotient_add_rank` `Nat.instAtLeastTwoHAddOfNat` `rank_subsingleton` `one_add_one_eq_two` `Cardinal.instCharZero`

---

← Back to Index