mem_carrier_iff — Mathlib

English

Variant of mem_carrier_iff_of_mem_mul specialized to non-multiplied degrees, giving a direct equivalence with HomogeneousLocalization terms.

Русский

Специализированная версия mem_carrier_iff_of_mem_mul для неумноженных степеней, даёт прямое эквивалентность с терминами HomogeneousLocalization.

LaTeX

$$$\text{mem_carrier_iff_of_mem}$(hm, q, a, hn)$$

Lean4

theorem mem_carrier_iff (q : Spec.T A⁰_ f) (a : A) :
    a ∈ carrier f_deg q ↔
      ∀ i,
        (HomogeneousLocalization.mk
              ⟨m * i, ⟨proj 𝒜 i a ^ m, by rw [← smul_eq_mul]; mem_tac⟩, ⟨f ^ i, by rw [mul_comm]; mem_tac⟩, ⟨_, rfl⟩⟩ :
            A⁰_ f) ∈
          q.1 :=
  Iff.rfl

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