mathlib3
5a1fa97e - chore(number_theory/pell): golf, use tactic mode (#18091)

Commit

2 years ago

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

Author

urkud

Parents