Theorem Basis.exists_opNorm_le

Modification history

2025-07-24 16:31

Mathlib/Analysis/Normed/Module/FiniteDimension.lean

chore: rename `Basis` to `Module.Basis` (#27381) …

Deleted Basis.exists_opNorm_le View on Github →

2024-02-04 13:16

Mathlib/Analysis/NormedSpace/FiniteDimension.lean

chore: rename op_norm to opNorm (#10185)

Added Basis.exists_opNorm_le View on Github →