mathlib3
3ec899aa - chore(topology/algebra): bundled homs in group and ring completion (#8497)

Commit

4 years ago

chore(topology/algebra): bundled homs in group and ring completion (#8497) Also take the opportunity to remove is_Z_bilin (who was scheduled for removal from the beginning).

Author

PatrickMassot

Parents

189e90ea

mathlib3 3ec899aa - chore(topology/algebra): bundled homs in group and ring completion (#8497)

mathlib3
3ec899aa - chore(topology/algebra): bundled homs in group and ring completion (#8497)