Def CompleteLatticeHom.OrderIso.toCompleteLatticeHom

Modification history

2026-07-08 18:17
Mathlib/Order/Hom/CompleteLattice.lean
feat(Translate): validate all translations (#40365) …
Added CompleteLatticeHom.OrderIso.toCompleteLatticeHomView on Github →