Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_multilinear_map.mk_pi_ring_apply_one_eq_self

Modification history

2020-10-12 14:57
src/analysis/normed_space/multilinear.lean
feat(analysis/normed_space/multilinear): define `mk_pi_algebra` (#4316) …
Deleted continuous_multilinear_map.mk_pi_ring_apply_one_eq_selfView on Github →
2020-02-07 16:57
src/analysis/normed_space/multilinear.lean
feat(analysis/normed_space/multilinear): norm on continuous multilinear maps (#1956) …
Added continuous_multilinear_map.mk_pi_ring_apply_one_eq_selfView on Github →