Commit 2023-05-23 10:39 91d9c139

View on Github →

feat: port RingTheory.Henselian (#4260)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Henselian.lean

added theorem HenselianLocalRing.TFAE

added theorem isLocalRingHom_of_le_jacobson_bot