Commit 2024-10-17 14:30 d82cdbff

View on Github →

feat(RingTheory/Smooth): Smoothness of product rings. (#15131)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Pi.lean

added def Pi.algHom

Modified Mathlib/RingTheory/Ideal/QuotientOperations.lean

added theorem Ideal.ker_quotientMap_mk

Created Mathlib/RingTheory/Smooth/Pi.lean

added theorem Algebra.FormallySmooth.of_pi

added theorem Algebra.FormallySmooth.pi_iff