mathlib
35c1956c - refactor(number_theory/pell): Small golf using `int.eq_of_mul_eq_one` (#18505)

Commit

2 years ago

refactor(number_theory/pell): Small golf using `int.eq_of_mul_eq_one` (#18505) This is a small golf using `int.eq_of_mul_eq_one`.

Author

tb65536

Parents