Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2020-06-04 15:38
7d803a98
View on Github →
feat(topology/metric_space/isometry): group structure on isometries (
#2950
) Closes
#2908
Estimated changes
Modified
src/topology/metric_space/isometry.lean
added
theorem
isometric.apply_inv_self
added
theorem
isometric.coe_mul
added
theorem
isometric.coe_one
added
theorem
isometric.inv_apply_self
added
theorem
isometric.mul_apply