Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-15 08:11 585d6419

View on Github →

refactor(linear_algebra/basic): split file (#12637) linear_algebra.basic has become a 2800 line monster, with lots of imports. This is some further work on splitting it into smaller pieces, by extracting everything about (or needing) span to linear_algebra.span.

Estimated changes

deleted def linear_equiv.coord
deleted theorem linear_equiv.coord_self
deleted theorem linear_map.eq_on_span'
deleted theorem linear_map.eq_on_span
deleted theorem linear_map.ext_on
deleted theorem linear_map.ext_on_range
deleted theorem linear_map.map_eq_top_iff
deleted theorem linear_map.map_injective
deleted theorem submodule.coe_sup
deleted theorem submodule.comap_map_eq
deleted theorem submodule.map_span
deleted theorem submodule.map_span_le
deleted theorem submodule.mem_prod
deleted theorem submodule.mem_span
deleted theorem submodule.mem_span_insert
deleted theorem submodule.mem_sup'
deleted theorem submodule.mem_sup
deleted theorem submodule.mem_supr
deleted def submodule.prod
deleted theorem submodule.prod_bot
deleted theorem submodule.prod_coe
deleted theorem submodule.prod_inf_prod
deleted theorem submodule.prod_mono
deleted theorem submodule.prod_sup_prod
deleted theorem submodule.prod_top
deleted def submodule.span
deleted theorem submodule.span_Union
deleted theorem submodule.span_empty
deleted theorem submodule.span_eq
deleted theorem submodule.span_eq_bot
deleted theorem submodule.span_eq_of_le
deleted theorem submodule.span_image
deleted theorem submodule.span_induction'
deleted theorem submodule.span_induction
deleted theorem submodule.span_insert
deleted theorem submodule.span_int_eq
deleted theorem submodule.span_le
deleted theorem submodule.span_mono
deleted theorem submodule.span_nat_eq
deleted theorem submodule.span_neg
deleted theorem submodule.span_prod_le
deleted theorem submodule.span_smul_le
deleted theorem submodule.span_span
deleted theorem submodule.span_sup
deleted theorem submodule.span_union
deleted theorem submodule.span_univ
deleted theorem submodule.span_zero
deleted theorem submodule.subset_span
deleted theorem submodule.sup_span
deleted theorem submodule.supr_eq_span
deleted theorem submodule.supr_induction'
deleted theorem submodule.supr_induction
added theorem linear_map.eq_on_span'
added theorem linear_map.eq_on_span
added theorem linear_map.ext_on
added theorem submodule.coe_sup
added theorem submodule.comap_map_eq
added theorem submodule.map_span
added theorem submodule.map_span_le
added theorem submodule.mem_prod
added theorem submodule.mem_span
added theorem submodule.mem_sup'
added theorem submodule.mem_sup
added theorem submodule.mem_supr
added def submodule.prod
added theorem submodule.prod_bot
added theorem submodule.prod_coe
added theorem submodule.prod_mono
added theorem submodule.prod_top
added def submodule.span
added theorem submodule.span_Union
added theorem submodule.span_empty
added theorem submodule.span_eq
added theorem submodule.span_eq_bot
added theorem submodule.span_image
added theorem submodule.span_insert
added theorem submodule.span_int_eq
added theorem submodule.span_le
added theorem submodule.span_mono
added theorem submodule.span_nat_eq
added theorem submodule.span_neg
added theorem submodule.span_prod_le
added theorem submodule.span_smul_le
added theorem submodule.span_span
added theorem submodule.span_sup
added theorem submodule.span_union
added theorem submodule.span_univ
added theorem submodule.span_zero
added theorem submodule.subset_span
added theorem submodule.sup_span
added theorem submodule.supr_eq_span