Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-06 19:04 edd29d0f

View on Github →

chore(ring_theory/power_series): weaken assumptions for nontrivial (#3301)

Estimated changes

Modified src/logic/nontrivial.lean

Modified src/ring_theory/power_series.lean

modified theorem mv_power_series.X_inj