Theorem ClosedSubmodule.mem_orthogonal_iff

Modification history

2026-01-27 22:28

Mathlib/Analysis/InnerProductSpace/Orthogonal.lean

chore(Analysis/InnerProductSpace/Orthogonal): add simp attrib, rename (#34103) …

Deleted ClosedSubmodule.mem_orthogonal_iff View on Github →

2026-01-17 20:29

Mathlib/Analysis/InnerProductSpace/Orthogonal.lean

feat(Analysis/InnerProductSpace/Orthogonal): add duplicates for `ClosedSubmodule` (#29241) …

Added ClosedSubmodule.mem_orthogonal_iff View on Github →