Theorem SeparationQuotient.mk_eq_one_iff

Modification history

2024-11-15 20:09
Mathlib/Analysis/Normed/Group/Uniform.lean
feat(Analysis/InnerProductSpace/Dual, Analysis/Normed/Group/SeparationQuotient): add null subspaces (#16707) …
Added SeparationQuotient.mk_eq_one_iffView on Github →