Commit 2024-10-03 17:44 2d5610a7

View on Github →

feat(RingTheory/Unramified): Formally unramified product of rings (#15141)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Ring/Idempotents.lean

added theorem IsIdempotentElem.map

added theorem IsIdempotentElem.mul

Modified Mathlib/RingTheory/Unramified/Basic.lean

added theorem Algebra.FormallyUnramified.of_surjective

Created Mathlib/RingTheory/Unramified/Pi.lean

added theorem Algebra.FormallyUnramified.pi_iff