Mathlib v3 is deprecated. Go to Mathlib v4

Theorem affine_isometry.angle_map

Modification history

2023-03-24 21:41
src/geometry/euclidean/angle/unoriented/affine.lean
refactor(analysis/inner_product_space/basic): do not extend normed_add_comm_group (#18583) …
Modified affine_isometry.angle_mapView on Github →
2022-10-13 06:01
src/geometry/euclidean/angle/unoriented/affine.lean
refactor(geometry/euclidean): split up unoriented angles (#16942) …
Modified affine_isometry.angle_mapView on Github →
2022-09-05 03:19
src/geometry/euclidean/basic.lean
feat(geometry/euclidean/basic): `affine_isometry.angle_map` (#16374) …
Added affine_isometry.angle_mapView on Github →