mathlib3
22eba86c - feat(*): add some missing `coe_*` lemmas (#6697)

Commit
4 years ago
feat(*): add some missing `coe_*` lemmas (#6697) * add `submonoid.coe_pow`, `submonoid.coe_list_prod`, `submonoid.coe_multiset_prod`, `submonoid.coe_finset_prod`, `subring.coe_pow`, `subring.coe_nat_cast`, `subring.coe_int_cast`; * add `rat.num_div_denom`; * add `inv_of_pow`.
Author
Parents
Loading