Theorem Algebra.FormallyUnramified.pi_iff

Modification history

2024-10-03 17:44
Mathlib/RingTheory/Unramified/Pi.lean
feat(RingTheory/Unramified): Formally unramified product of rings (#15141)
Added Algebra.FormallyUnramified.pi_iffView on Github →