Theorem Real.isometry_intCast

Modification history

2026-04-15 08:53
Mathlib/Analysis/Normed/Group/Uniform.lean
feat(Topology/Algebra/Group/Matrix): refactor; continuity of maps on GL(n) and SL(n) (#37601) …
Added Real.isometry_intCastView on Github →