[Merged by Bors] - fix: fix Q-smul diamond in Complex#5341
[Merged by Bors] - fix: fix Q-smul diamond in Complex#5341ChrisHughes24 wants to merge 13 commits intomasterfrom
Conversation
Mathlib/Data/Complex/Basic.lean
Outdated
|
|
||
| noncomputable instance : Field ℂ := | ||
| { inv := Inv.inv | ||
| { qsmul := fun n z => ⟨n • z.re - 0 * z.im, n • z.im + 0 * z.re⟩ |
There was a problem hiding this comment.
Please add a note here why we have the weird definition?
There was a problem hiding this comment.
I added a comment, but I actually don't understand the comment to do with RestrictScalars on the instance in Data.Complex.Module, so I don't fully understand the reason behind this change.
There was a problem hiding this comment.
I should maybe improve that comment as well.
There was a problem hiding this comment.
I just realised I could also change the definition of Field to this, and change the ratCast def to go through the reals. This also makes the instance diagram commute, but for a more complex reason.
noncomputable instance : Field ℂ :=
{ ratCast := fun q => (q : ℝ)
ratCast_mk := fun a b h1 h2 => by
show ofReal' _ = _
simp [Rat.cast_mk' a b h1 h2]; rfl
inv := Inv.inv
mul_inv_cancel := @Complex.mul_inv_cancel
inv_zero := Complex.inv_zero }|
@eric-wieser I know you're not a fan of the weird definition of docs#Module.complexToReal for nice defeqs, so I thought you may want to see this. |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
bors merge |
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
The example that has now been added to
Data.Complex.Moduledid not commute before, but now that the definition ofqsmulin theFieldinstance for complex numbers has been changed, it does commute.I also fixed the statement of
rat_cast_re, so it's an equality of real numbers now, without a coercion to complex. I also restored thenorm_castattribute onrat_cast_imandrat_cast_resince there is no error, probably because the coercion toComplexhas been removed.