Theorem Algebra.FormallySmooth.of_pi

Modification history

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