mathlib

6b647c3b - refactor(linear_algebra, analysis/inner_product_space): use `⊤ ≤` instead of `= ⊤` in bases constructors (#15697)

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