multipliable_int_iff_multipliable_nat_and_neg

English

Analogous equivalence with f(-n).

Русский

Аналогичная эквивалентность с f(-n).

LaTeX

$$$\\displaystyle \\text{Multipliable}(f) \\iff \\bigl(\\text{Multipliable}(n\\mapsto f(n)) \\land \\text{Multipliable}(n\\mapsto f(-n))\\bigr)$$$

Lean4

/-- "iff" version of `Multipliable.of_nat_of_neg`. -/
@[to_additive /-- "iff" version of `Summable.of_nat_of_neg`. -/
    ]
theorem multipliable_int_iff_multipliable_nat_and_neg {f : ℤ → G} :
    Multipliable f ↔ (Multipliable fun n : ℕ ↦ f n) ∧ (Multipliable fun n : ℕ ↦ f (-n)) :=
  by
  refine ⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Multipliable.of_nat_of_neg hf₁ hf₂⟩ <;> apply p.comp_injective
  exacts [Nat.cast_injective, neg_injective.comp Nat.cast_injective]
    -- We're not really using the ring structure here:
    -- we only use multiplication by `-1`, so perhaps this can be generalised further.

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