mathlib
802513cb - feat(ring_theory/adjoin_root): a bit of missing API for maps between certain quotients of `adjoin_root f` (#15757)

Commit

3 years ago

feat(ring_theory/adjoin_root): a bit of missing API for maps between certain quotients of `adjoin_root f` (#15757) A few lemmas needed for #15000. Co-authored-by: Anne Baanen.

Author

Paul-Lez

Parents

811da369

mathlib 802513cb - feat(ring_theory/adjoin_root): a bit of missing API for maps between certain quotients of `adjoin_root f` (#15757)

mathlib
802513cb - feat(ring_theory/adjoin_root): a bit of missing API for maps between certain quotients of `adjoin_root f` (#15757)