map_ofList — Mathlib

English

There exists a linear equivalence between M modulo (r :: rs) and (QuotSMulTop r M) modulo (Ideal.ofList rs · ⊤).

Русский

Существует линейное эквивалентное отображение между M/(r :: rs) и (M / rs) / r·(M / rs).

LaTeX

$$$\\left(M \\Big\\slash (\\text{Ideal.ofList} (r :: rs) \\;\\top)\\right) \\cong_{R} \\left( \\; \\text{QuotSMulTop } r M \\Big/ (\\text{Ideal.ofList } rs \\;\\top) \\right)$$$

Lean4

@[simp]
theorem map_ofList (f : R →+* S) (rs : List R) : map f (ofList rs) = ofList (rs.map f) :=
  Eq.trans (map_span f {r | r ∈ rs}) <| congrArg span <| Set.ext (fun _ => List.mem_map.symm)

Похожие утверждения