Mathlib Changelog
v4
Changelog
About
Github
Theorem
RingHom.Etale.containsIdentities
Modification history
2026-02-10 11:38
Mathlib/RingTheory/RingHom/Etale.lean
refactor(AlgebraicGeometry/Smooth): replace `Locally IsStandardSmooth` by `Smooth` (#35034) …
Added
RingHom.Etale.containsIdentities
View on Github →