Commit 2025-03-11 09:45 58255dfa

View on Github →

feat(LinearIndependent): more API for linearIndepOn (#22368) We add a few more API lemmas for linearIndepOn, in many cases generalizing id versions of existing lemmas to arbitrary functions.

Estimated changes

Modified Mathlib/LinearAlgebra/Dimension/Constructions.lean

added theorem LinearIndepOn.quotient_iff_union

added theorem LinearIndepOn.union_id_of_quotient

modified theorem LinearIndepOn.union_of_quotient

added theorem linearIndepOn_union_iff_quotient

Modified Mathlib/LinearAlgebra/Dimension/RankNullity.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Basic.lean

added theorem LinearIndepOn.congr

modified theorem LinearIndepOn.id_union

deleted theorem LinearIndepOn.singleton

added theorem LinearIndepOn.union

added theorem LinearIndepOn_iff_linearIndepOn_image_injOn

added theorem linearIndepOn_congr

added theorem linearIndepOn_id_union_iff

added theorem linearIndepOn_singleton_iff

added theorem linearIndepOn_union_iff

Modified Mathlib/LinearAlgebra/LinearIndependent/Defs.lean

added theorem LinearIndepOn.zero_not_mem_image

added theorem linearIndepOn_zero_iff

Modified Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

added theorem LinearIndepOn.mem_span_iff

added theorem LinearIndepOn.mem_span_iff_id

added theorem LinearIndepOn.not_mem_span_iff

added theorem LinearIndepOn.not_mem_span_iff_id

added theorem linearIndepOn_id_insert_iff

added theorem linearIndepOn_insert_iff

added theorem linearIndepOn_pair_iff

Modified Mathlib/LinearAlgebra/Span/Defs.lean

added theorem Disjoint.of_span

added theorem Disjoint.of_span₀