Theorem CategoryTheory.OrthogonalReflection.iteration_map_succ_injectivity

Modification history

2025-12-08 05:19
Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean
refactor: `Ordinal.toType` → `Ordinal.ToType` (#32449) …
Modified CategoryTheory.OrthogonalReflection.iteration_map_succ_injectivityView on Github →
2025-12-01 18:53
Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean
feat(CategoryTheory): localization of locally presentable categories (#30554) …
Added CategoryTheory.OrthogonalReflection.iteration_map_succ_injectivityView on Github →