Def adjoin_root.quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk
Modification history
2022-03-23 12:35
src/ring_theory/adjoin_root.lean
feat(ring_theory/polynomial/basic): the isomorphism between `R[a]/I[a]` and `(R/I[X])/(f mod I)` for `a` a root of polynomial `f` and `I` and ideal of `R` (#12646) …
Added adjoin_root.quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mkView on Github →