coe_factor_orderIso_map_eq_one_iff

English

Under an order isomorphism d between divisor lattices, the image of (u, hu') equals 1 in the codomain iff u equals 1.

Русский

При отображении-изоморфизме между цепями делителей образ (u, hu') равен единице тогда и только тогда, когда u равно единице.

LaTeX

$$$(d \langle u, hu'\rangle) = 1 \iff u = 1$$$

Lean4

theorem coe_factor_orderIso_map_eq_one_iff {m u : Associates M} {n : Associates N} (hu' : u ≤ m)
    (d : Set.Iic m ≃o Set.Iic n) : (d ⟨u, hu'⟩ : Associates N) = 1 ↔ u = 1 :=
  ⟨fun hu =>
    by
    rw [show u = (d.symm ⟨d ⟨u, hu'⟩, (d ⟨u, hu'⟩).prop⟩) by
        simp only [Subtype.coe_eta, OrderIso.symm_apply_apply, Subtype.coe_mk]]
    conv_rhs => rw [← factor_orderIso_map_one_eq_bot d.symm]
    congr, fun hu => by
    simp_rw [hu]
    conv_rhs => rw [← factor_orderIso_map_one_eq_bot d]
    rfl⟩

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