Theorem Algebra.FormallySmooth.pi_iff

Modification history

2024-10-17 14:30
Mathlib/RingTheory/Smooth/Pi.lean
feat(RingTheory/Smooth): Smoothness of product rings. (#15131)
Added Algebra.FormallySmooth.pi_iffView on Github →