Def OrderIso.toCompleteLatticeHom

Modification history

2024-01-16 21:01

Mathlib/Order/Hom/CompleteLattice.lean

feat: basic theory connecting `R[X]`-submodules and invariant `R`-submodules (#9721)

Added OrderIso.toCompleteLatticeHom View on Github →