Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-05 19:08 8b2d1815

View on Github →

feat(ring_theory/laurent_series): laurent_series is_fraction_ring over power_series (#11220)

Estimated changes

Modified src/ring_theory/laurent_series.lean

Modified src/ring_theory/localization.lean

added theorem is_localization.of_le

Modified src/ring_theory/non_zero_divisors.lean

added theorem is_unit_of_mem_non_zero_divisors

Modified src/ring_theory/power_series/basic.lean

added theorem power_series.X_ne_zero