[Merged by Bors] - chore(data/complex/basic): upgrade complex.norm_sq to a monoid_with_zero_hom
#5553
Conversation
urkud
commented
Jan 1, 2021
urkud
commented
| @[simp] lemma norm_sq_I : norm_sq I = 1 := by simp [norm_sq] | ||
|
|
||
| lemma norm_sq_nonneg (z : ℂ) : 0 ≤ norm_sq z := | ||
| add_nonneg (mul_self_nonneg _) (mul_self_nonneg _) | ||
|
|
||
| @[simp] lemma norm_sq_eq_zero {z : ℂ} : norm_sq z = 0 ↔ z = 0 := | ||
| lemma norm_sq_eq_zero {z : ℂ} : norm_sq z = 0 ↔ z = 0 := |
There was a problem hiding this comment.
Is this lemma somewhere in monoid_with_zero_hom too?
There was a problem hiding this comment.
Yes but the proof of complex.field depends on complex.norm_sq_eq_zero, so we can't reuse the proof.
There was a problem hiding this comment.
Just giving a more explicit explanation for my own benefit: monoid_with_zero_hom.map_eq_zero requires the domain of the monoid_with_zero_hom to be a group_with_zero, but that instance for ℂ requires this result about norm_sq.
The proof used here relies instead on the fact that ℝ is a linear_ordered_ring.
| @[simp] lemma norm_sq_I : norm_sq I = 1 := by simp [norm_sq] | ||
|
|
||
| lemma norm_sq_nonneg (z : ℂ) : 0 ≤ norm_sq z := | ||
| add_nonneg (mul_self_nonneg _) (mul_self_nonneg _) | ||
|
|
||
| @[simp] lemma norm_sq_eq_zero {z : ℂ} : norm_sq z = 0 ↔ z = 0 := | ||
| lemma norm_sq_eq_zero {z : ℂ} : norm_sq z = 0 ↔ z = 0 := |
There was a problem hiding this comment.
Just giving a more explicit explanation for my own benefit: monoid_with_zero_hom.map_eq_zero requires the domain of the monoid_with_zero_hom to be a group_with_zero, but that instance for ℂ requires this result about norm_sq.
The proof used here relies instead on the fact that ℝ is a linear_ordered_ring.
github-actions
bot
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded! And happy new year! 🎉 |
bors
bot
changed the title
complex.norm_sq to a monoid_with_zero_homcomplex.norm_sq to a monoid_with_zero_hom
