Theorem AffineIsometryEquiv.trans_assoc

Modification history

2026-09-28 17:33
Mathlib/Analysis/Normed/Affine/Isometry.lean
perf(Analysis/Normed/Affine/Isometry): scope the V₄/P₄ and V₁'/P₁' variables to their users (#42246) …
Modified AffineIsometryEquiv.trans_assocView on Github →
2023-05-19 18:00
Mathlib/Analysis/NormedSpace/AffineIsometry.lean
feat: port Analysis.NormedSpace.AffineIsometry (#3651)
Added AffineIsometryEquiv.trans_assocView on Github →