Commit 2024-11-15 15:51 9127890b

View on Github →

chore(LinearAlgebra/Span): split off definition of Submodule.span (#18618) This PR creates a new file LinearAlgebra.Span.Defs which contains the definition of a submodule span and some elementary results. Everything that needs heavier imports gets moved to LinearAlgebra.Span.Basic.

Estimated changes

deleted theorem Submodule.coe_sup
deleted theorem Submodule.iSup_eq_span
deleted theorem Submodule.iSup_span
deleted theorem Submodule.mem_iSup
deleted theorem Submodule.mem_sSup
deleted theorem Submodule.mem_span
deleted theorem Submodule.mem_span_insert
deleted theorem Submodule.mem_span_pair
deleted theorem Submodule.mem_sup'
deleted theorem Submodule.mem_sup
deleted def Submodule.span
deleted theorem Submodule.span_closure
deleted theorem Submodule.span_empty
deleted theorem Submodule.span_eq
deleted theorem Submodule.span_eq_bot
deleted theorem Submodule.span_eq_closure
deleted theorem Submodule.span_eq_of_le
deleted theorem Submodule.span_eq_span
deleted theorem Submodule.span_iUnion
deleted theorem Submodule.span_iUnion₂
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_monotone
deleted theorem Submodule.span_nat_eq
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
added theorem Submodule.coe_sup
added theorem Submodule.iSup_eq_span
added theorem Submodule.iSup_span
added theorem Submodule.mem_iSup
added theorem Submodule.mem_sSup
added theorem Submodule.mem_span
added theorem Submodule.mem_sup'
added theorem Submodule.mem_sup
added def Submodule.span
added theorem Submodule.span_closure
added theorem Submodule.span_empty
added theorem Submodule.span_eq
added theorem Submodule.span_eq_bot
added theorem Submodule.span_eq_span
added theorem Submodule.span_iUnion
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_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