Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_basis.op_norm_le

Modification history

2021-05-10 07:36

src/analysis/normed_space/finite_dimension.lean

refactor(*): bundle `is_basis` (#7496) …

Deleted is_basis.op_norm_le View on Github →

2020-09-12 18:30

src/analysis/normed_space/finite_dimension.lean

feat(normed_space): second countability for linear maps (#4099) …

Added is_basis.op_norm_le View on Github →