Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-08 00:31 5a1fa97e

View on Github →

chore(number_theory/pell): golf, use tactic mode (#18091) Also drop an unneeded assumption in pell.eq_pow_of_pell_lem.

Estimated changes

modified theorem pell.eq_pow_of_pell
modified theorem pell.eq_pow_of_pell_lem