Commit 2022-07-29 02:07 6b647c3b

refactor(linear_algebra, analysis/inner_product_space): use ⊤ ≤ instead of = ⊤ in bases constructors (#15697) All the existing proof just need a .ge to be fixed, and this allows to remove a lot of rw [eq_top_iff], and it sticks with the convention of having weakest forms in assumptions and stronger forms in conclusion. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60.E2.8A.A4.20.E2.89.A4.20span.60.20in.20basis.20constructors