map_subtype_coe_factors' — Mathlib

English

The map of factors' a to Coe, equals the map of factors a via the embedding mk into Associates.

Русский

Образ факторов a через отображение коэффициента равен образу факторов a через вложение mk в Associates.

LaTeX

$$(factors' a).map (↑) = (factors a).map Associates.mk$$

Lean4

@[simp]
theorem map_subtype_coe_factors' {a : α} : (factors' a).map (↑) = (factors a).map Associates.mk := by
  simp [factors', Multiset.map_pmap, Multiset.pmap_eq_map]

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