Commit 2024-10-28 09:08 fb052069

View on Github →

feat(RingTheory/Ideal/Maps): lemmas of ring isomorphisms act on ideals (#18249) Add some lemmas of ring isomorphisms act on ideals, for example, prove that if e : R ≃+* S is a ring isomorphism, p is an ideal of R, p is prime(resp. maximal), then Ideal.map e p is prime(resp. maximal).

Estimated changes

modified theorem Ideal.comap_of_equiv
modified theorem Ideal.comap_symm
modified theorem Ideal.map_comap_of_equiv
modified theorem Ideal.map_of_equiv
modified theorem Ideal.map_symm
added theorem Ideal.mem_map_of_equiv