basic): add adjoin_induction' and adjoin_adjoin_coe_preimage (#10427)

Commit

4 years ago

feat(ring_theory/adjoin/basic): add adjoin_induction' and adjoin_adjoin_coe_preimage (#10427) From FLT-regular. Co-authored-by: Chris Birkbeck <cd.birkbeck@gmail.com>

Author

riccardobrasca

Parents

c192937f

mathlib3 0cbba1a4 - feat(ring_theory/adjoin/basic): add adjoin_induction' and adjoin_adjoin_coe_preimage (#10427)

mathlib3
0cbba1a4 - feat(ring_theory/adjoin/basic): add adjoin_induction' and adjoin_adjoin_coe_preimage (#10427)