mathlib

mathlib copied to clipboard

This makes a number of changes:

• It avoids the use of refine_struct to define real.comm_ring. This is useful for porting, as that tactic no longer exists. The new proof is also very simple.
• It provides some missing lemmas about pow and smul linking to cauchy sequences
• It redefines has_smul and has_pow on real in a way that is compatible with cauchy sequences. This:
  • makes the pow and smul lemmas above easier
  • means we only need a single smul lemma rather than separate nsmul, zsmul, qsmul lemmas.
  • makes ((2 / 3 : ℚ) • 3 : ℝ) "computable" since it doesn't go through real.division_ring any more
  • has some minor downsides: pow_zero, rat.smul_def, and zpow_coe_nat are no longer true by definition. The proofs this breaks are already changed as of #18136.

---

• [x] depends on: #18118
• [x] depends on: #18129
• [x] depends on: #18156
• [x] depends on: #18225

:v: eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

I'm a bit confused: is the has_pow instance changing (up to defeq) or not? If so then why?

I'm a bit confused: is the has_pow instance changing (up to defeq) or not?

Yes; the new definition is "elementwise power on the cauchy sequence"

If so then why?

Mainly because it makes the proof easier. Do you feel strongly about the defeqs listed in #18136 being useful?

Note that #18156 is a bugfix for pi.has_pow independently of this PR; ring broke on real not because I changed the defeq of has_pow, but because I changed the syntactic instance that was found.

Yes, I think it is definitely better to have a useful definition of ^ than to save a few lines in the internals of real.

I can restore the old has_pow then; it's the has_smul defeq change that's more useful anyway.

I suggest we abandon this given that it seems to work better in Lean 4 to use a CommRing instance like the present mathlib 3 one.

This PR/issue depends on:

• ~~leanprover-community/mathlib#18118~~
• ~~leanprover-community/mathlib#18129~~
• ~~leanprover-community/mathlib#18156~~
• ~~leanprover-community/mathlib#18225~~ By Dependent Issues (🤖). Happy coding!