Def nullSubmodule

Modification history

2024-11-15 20:09

Mathlib/Analysis/Normed/Group/NullSubmodule.lean

feat(Analysis/InnerProductSpace/Dual, Analysis/Normed/Group/SeparationQuotient): add null subspaces (#16707) …

Added nullSubmodule View on Github →