Def OrderIso.toCompleteLatticeHom

Modification history

2026-07-08 18:17
Mathlib/Order/Hom/CompleteLattice.lean
feat(Translate): validate all translations (#40365) …
Deleted OrderIso.toCompleteLatticeHomView on Github →
2024-01-16 21:01
Mathlib/Order/Hom/CompleteLattice.lean
feat: basic theory connecting `R[X]`-submodules and invariant `R`-submodules (#9721)
Added OrderIso.toCompleteLatticeHomView on Github →