mathlib3
c0421e76 - feat({ring_theory,group_theory}/localization): add some small lemmas for localisation API (#12861)

Commit
3 years ago
feat({ring_theory,group_theory}/localization): add some small lemmas for localisation API (#12861) Add the following: * `sub_mk`: a/b - c/d = (ad - bc)/(bd) * `mk_pow`: (a/b)^n = a^n/b^n * `mk_int_cast`, `mk_nat_cast`: m = m/1 for integer/natural number m.
Author
Parents
Loading