Commit 2025-05-09 19:38 7a5d26af

View on Github →

feat: IsometryClass (#18754)

Estimated changes

Modified Mathlib/Analysis/Normed/Group/Uniform.lean

added theorem nnnorm_map'

added theorem norm_map'

Modified Mathlib/Topology/MetricSpace/Isometry.lean

added theorem IsometryClass.coe_coe

added theorem IsometryClass.diam_image

added theorem IsometryClass.diam_range

added theorem IsometryClass.ediam_image

added theorem IsometryClass.ediam_range

added def IsometryClass.toIsometryEquiv

added theorem IsometryClass.toIsometryEquiv_injective

Modified scripts/nolints_prime_decls.txt