chore(data/real/ennreal): add a few lemmas (#5071)

Also swap LHS with RHS in `to_real_mul_to_real` and rename it to `to_real_mul`.
leanprover-community · Nov 22, 2020 · 2044451 · 2044451
1 parent f627d76
commit 2044451
Show file tree

Hide file tree

Showing 3 changed files with 134 additions and 99 deletions.
diff --git a/src/analysis/normed_space/enorm.lean b/src/analysis/normed_space/enorm.lean
@@ -184,6 +184,6 @@ lemma finite_norm_eq (x : e.finite_subspace) : ∥x∥ = (e x).to_real := rfl
 
 /-- Normed space instance on `e.finite_subspace`. -/
 instance : normed_space 𝕜 e.finite_subspace :=
-{ norm_smul_le := λ c x, le_of_eq $ by simp [finite_norm_eq, ← ennreal.to_real_mul_to_real] }
+{ norm_smul_le := λ c x, le_of_eq $ by simp [finite_norm_eq, ennreal.to_real_mul] }
 
 end enorm