Theorem InnerProductSpace.nullSubmodule_le_ker_toDualMap_right

Modification history

2025-12-27 09:40

Mathlib/Analysis/InnerProductSpace/Dual.lean

chore(*): restrict operations to `LinearMap`s (#33241) …

Modified InnerProductSpace.nullSubmodule_le_ker_toDualMap_right View on Github →

2024-11-15 20:09

Mathlib/Analysis/InnerProductSpace/Dual.lean

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

Added InnerProductSpace.nullSubmodule_le_ker_toDualMap_right View on Github →