Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-30 16:11 8ec7fcf8

View on Github →

feat(ring_theory/henselian): Henselian local rings (#8986)

Estimated changes

Modified src/algebra/ring/basic.lean

added theorem ring.inverse_mul_cancel

added theorem ring.inverse_mul_cancel_left

added theorem ring.inverse_mul_cancel_right

added theorem ring.mul_inverse_cancel

added theorem ring.mul_inverse_cancel_left

added theorem ring.mul_inverse_cancel_right

Created src/ring_theory/henselian.lean

added theorem henselian_local_ring.tfae

added theorem is_local_ring_hom_of_le_jacobson_bot