Def TwoSidedIdeal.orderIsoIsTwoSided

Modification history

2025-05-01 12:28
Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
chore: whitespace still (#24501) …
Modified TwoSidedIdeal.orderIsoIsTwoSidedView on Github →
2025-05-01 06:42
Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
feat: preliminaries for Wedderburn–Artin (#24119)
Added TwoSidedIdeal.orderIsoIsTwoSidedView on Github →