Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-17 14:37 ae610a04

View on Github →

feat(ring_theory/adjoin_root): adjoin roots to polynomials (#603)

Estimated changes

Created src/ring_theory/adjoin_root.lean

added def adjoin_root.adjoin_root

added theorem adjoin_root.coe_injective

added theorem adjoin_root.eval₂_root

added theorem adjoin_root.is_root_root

added def adjoin_root.lift

added theorem adjoin_root.lift_mk

added theorem adjoin_root.lift_of

added theorem adjoin_root.lift_root

added def adjoin_root.mk

added theorem adjoin_root.mk_self

added theorem adjoin_root.mul_div_root_cancel

added def adjoin_root.of

added def adjoin_root.root