Commit 2025-11-12 09:50 2dcdfaa5

View on Github →

feat: add an element to a linear indep family, more general version (#31515)

Estimated changes

Modified Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean

Modified Mathlib/Geometry/Euclidean/Altitude.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

Modified Mathlib/LinearAlgebra/Dimension/Constructions.lean

Modified Mathlib/LinearAlgebra/Dimension/RankNullity.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Basic.lean

deleted theorem LinearIndepOn.id_singleton

modified theorem linearIndepOn_singleton_iff

modified theorem linearIndependent_unique_iff

Modified Mathlib/LinearAlgebra/LinearIndependent/Defs.lean

added theorem LinearIndepOn.id_singleton

added theorem LinearIndepOn.singleton'

added theorem LinearIndepOn.singleton

added theorem LinearIndependent.of_subsingleton'

added theorem LinearIndependent.of_subsingleton

Modified Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

added theorem LinearIndepOn.id_insert'

added theorem LinearIndepOn.insert'

Modified Mathlib/LinearAlgebra/Span/Basic.lean

added theorem Submodule.disjoint_span_singleton''

modified theorem Submodule.disjoint_span_singleton'

Modified Mathlib/Topology/Category/Profinite/Nobeling/ZeroLimit.lean