Documentation Verification Report

Independence

📁 Source: Mathlib/LinearAlgebra/Projectivization/Independence.lean

Statistics

Metric	Count
Definitions `Dependent`	1
Theorems `dependent_iff`, `dependent_iff_not_independent`, `dependent_pair_iff_eq`, `independent_iff`, `independent_iff_iSupIndep`, `independent_iff_not_dependent`, `independent_pair_iff_ne`	7
Total	8

Projectivization

Definitions

Name	Category	Theorems
`Dependent` 📖	CompData	4 math math: `dependent_pair_iff_eq`, `independent_iff_not_dependent`, `dependent_iff`, `dependent_iff_not_independent`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dependent_iff` 📖	mathematical	—	`Dependent` `LinearIndependent` `Projectivization` `rep` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	—	`Mathlib.Tactic.Contrapose.contrapose₄` `inv_smul_smul` `LinearIndependent.units_smul` `exists_smul_eq_mk_rep` `rep_nonzero` `mk_rep`
`dependent_iff_not_independent` 📖	mathematical	—	`Dependent` `Independent`	—	`dependent_iff` `independent_iff`
`dependent_pair_iff_eq` 📖	mathematical	—	`Dependent` `Matrix.vecCons` `Projectivization` `Matrix.vecEmpty`	—	`dependent_iff_not_independent` `independent_iff` `linearIndependent_fin2` `rep_nonzero` `mk_eq_mk_iff'` `mk_rep`
`independent_iff` 📖	mathematical	—	`Independent` `LinearIndependent` `Projectivization` `rep` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	—	`LinearIndependent.units_smul` `exists_smul_eq_mk_rep` `rep_nonzero` `mk_rep`
`independent_iff_iSupIndep` 📖	mathematical	—	`Independent` `iSupIndep` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.completeLattice` `submodule`	—	`iSupIndep_iff_linearIndependent_of_ne_zero` `DivisionRing.isDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `independent_iff` `iSupIndep.linearIndependent` `submodule_eq` `Submodule.mem_span_singleton_self` `rep_nonzero`
`independent_iff_not_dependent` 📖	mathematical	—	`Independent` `Dependent`	—	`dependent_iff_not_independent`
`independent_pair_iff_ne` 📖	mathematical	—	`Independent` `Matrix.vecCons` `Projectivization` `Matrix.vecEmpty`	—	`independent_iff_not_dependent` `dependent_pair_iff_eq`

---

← Back to Index