Commit 2023-08-25 21:13 c085fa84

View on Github →

feat(LinearAlgebra/Basis): flag defined by a basis (#6269) Also add supporting lemmas and golf some proofs. Based on a file from the Sphere Eversion Project.

Estimated changes

added theorem Flag.mem_rangeFin
added def Flag.rangeFin
added def Basis.flag
added theorem Basis.flag_covby
added theorem Basis.flag_last
added theorem Basis.flag_le_iff
added theorem Basis.flag_mono
added theorem Basis.flag_strictMono
added theorem Basis.flag_succ
added theorem Basis.flag_wcovby
added theorem Basis.flag_zero
added theorem Basis.mem_toFlag
added theorem Basis.self_mem_flag
added def Basis.toFlag
modified theorem Submodule.span_insert