Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mul_self_le_mul_self_of_le_of_neg_le

Modification history

2019-08-08 02:35
src/algebra/ordered_ring.lean
feat (analysis/normed_space): Define real inner product space (#1248) …
Added mul_self_le_mul_self_of_le_of_neg_leView on Github →