Documentation Verification Report

LinearMap

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

Statistics

Metric	Count
Definitions `rank`	1
Theorems `le_rank_iff_exists_linearIndependent`, `le_rank_iff_exists_linearIndependent_finset`, `lift_rank_comp_le`, `lift_rank_comp_le_right`, `rank_add_le`, `rank_comp_le`, `rank_comp_le_left`, `rank_comp_le_right`, `rank_finset_sum_le`, `rank_le_domain`, `rank_le_range`, `rank_zero`	12
Total	13

LinearMap

Definitions

Name	Category	Theorems
`rank` 📖	CompOp	16 math math: `rank_le_domain`, `le_rank_iff_exists_linearIndependent`, `lift_rank_comp_le_right`, `rank_diagonal`, `rank_comp_le_left`, `InnerProductSpace.rank_rankOne`, `rank_le_range`, `rank_zero`, `rank_comp_le`, `rank_add_le`, `le_rank_iff_exists_linearIndependent_finset`, `rank_finset_sum_le`, `Matrix.rank_vecMulVec`, `isOpen_setOf_nat_le_rank`, `rank_comp_le_right`, `lift_rank_comp_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_rank_iff_exists_linearIndependent` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `rank` `DivisionRing.toRing` `Cardinal.lift` `Set.Elem` `LinearIndepOn` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike`	—	`RingHomSurjective.ids` `RingHomCompTriple.ids` `exists_rightInverse_of_surjective` `Module.Projective.of_free` `Module.Free.of_divisionRing` `range_rangeRestrict` `congr_fun` `le_rank_iff_exists_linearIndependent` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `Cardinal.mk_image_eq_lift` `LinearIndependent.map'` `Submodule.ker_subtype` `LinearIndepOn.image_of_comp` `LinearIndependent.of_comp` `Cardinal.mk_image_eq_of_injOn_lift` `Set.injOn_iff_injective` `LinearIndependent.injective` `LinearIndependent.cardinal_le_rank` `LinearIndepOn.id_image`
`le_rank_iff_exists_linearIndependent_finset` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Cardinal.instNatCast` `rank` `DivisionRing.toRing` `Finset.card` `LinearIndependent` `Set.Elem` `SetLike.coe` `Finset` `Finset.instSetLike` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `Set` `Set.instMembership`	—	`Cardinal.lift_natCast`
`lift_rank_comp_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Cardinal.lift` `rank` `comp` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Cardinal.instConditionallyCompleteLinearOrderBot`	—	`le_min` `RingHomCompTriple.ids` `Cardinal.lift_le` `rank_comp_le_left` `lift_rank_comp_le_right`
`lift_rank_comp_le_right` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Cardinal.lift` `rank` `comp` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	`RingHomCompTriple.ids` `rank.eq_1` `RingHomSurjective.ids` `range_comp` `lift_rank_map_le`
`rank_add_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `rank` `DivisionRing.toRing` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instAdd` `Cardinal.instAdd`	—	`RingHomSurjective.ids` `Submodule.rank_mono` `range_le_iff_comap` `Submodule.eq_top_iff'` `Submodule.mem_sup` `Submodule.rank_add_le_rank_add_rank` `DivisionRing.hasRankNullity`
`rank_comp_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `rank` `comp` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Cardinal.instConditionallyCompleteLinearOrderBot`	—	`RingHomCompTriple.ids` `Cardinal.lift_id` `lift_rank_comp_le`
`rank_comp_le_left` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `rank` `comp` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	`Submodule.rank_mono` `RingHomCompTriple.ids` `RingHomSurjective.ids` `range_comp` `map_le_range`
`rank_comp_le_right` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `rank` `comp` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	`RingHomCompTriple.ids` `Cardinal.lift_id` `lift_rank_comp_le_right`
`rank_finset_sum_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `rank` `DivisionRing.toRing` `Finset.sum` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `CommSemiring.toSemiring` `Cardinal.commSemiring`	—	`Finset.sum_hom_rel` `le_of_eq` `rank_zero` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `le_trans` `rank_add_le` `add_le_add_right` `Cardinal.addLeftMono`
`rank_le_domain` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `rank` `Module.rank` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`rank_range_le`
`rank_le_range` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `rank` `Module.rank` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`Submodule.rank_le`
`rank_zero` 📖	mathematical	—	`rank` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instZero` `Cardinal` `Cardinal.instZero`	—	`rank.eq_1` `range_zero` `rank_bot`

---

← Back to Index