Commit 2025-02-27 17:52 9ffa2f76

View on Github →

feat(RingTheory/SimpleRing/Congr): simpleness is preserved by ring isomorphism (#21292) A new file is created because SimpleRing/Basic contains a basic result RingHom.injective so that a new file is created to avoid a large amount of files importing Algebra/Ring/Equiv.lean and RingTheory/TwoSidedIdeal/Operations.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/SimpleRing/Congr.lean

added theorem IsSimpleRing.of_ringEquiv

added theorem IsSimpleRing.of_surjective

Modified Mathlib/RingTheory/TwoSidedIdeal/Operations.lean

added def RingEquiv.mapTwoSidedIdeal

added theorem RingEquiv.mapTwoSidedIdeal_apply

added theorem RingEquiv.mapTwoSidedIdeal_symm

modified def TwoSidedIdeal.comap

added theorem TwoSidedIdeal.comap_comap

added theorem TwoSidedIdeal.comap_le_comap