Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-29 20:31 89102286

View on Github →

chore(data/polynomial): use dot notation for sub lemmas (#13799) To match the additive versions

Estimated changes

Modified src/data/polynomial/monic.lean

added theorem polynomial.monic.sub_of_left

added theorem polynomial.monic.sub_of_right

deleted theorem polynomial.monic_sub_of_left

deleted theorem polynomial.monic_sub_of_right

Modified src/ring_theory/power_basis.lean