Theorem OrderHom.gfp_induction

Modification history

2024-11-23 05:51

Mathlib/Order/FixedPoints.lean

chore(Order/FixedPoints): remove adaptation notes for OrderHom regarding lean4 issue #1910 (#19380) …

Modified OrderHom.gfp_induction View on Github →

2022-12-23 15:45

Mathlib/Order/FixedPoints.lean

feat: port Order.FixedPoints (#1174)

Added OrderHom.gfp_induction View on Github →