Theorems · Theorem · commutative algebra

MvPowerSeries.tendsto_antidiagonal

∀ {M : Type u_3} {S : Type u_4} [inst : AddMonoid M] [inst_1 : Finset.HasAntidiagonal M] [inst_2 : NormedRing S]
  [IsUltrametricDist S] {C : M → ℝ},
  (∀ (a b : M), C (a + b) = C a * C b) →
    ∀ {f g : M → S},
      Filter.Tendsto (fun i => ‖f i‖ * C i) Filter.cofinite (nhds 0) →
        Filter.Tendsto (fun i => ‖g i‖ * C i) Filter.cofinite (nhds 0) →
          Filter.Tendsto (fun a => ‖∑ p ∈ Finset.HasAntidiagonal.antidiagonal a, f p.1 * g p.2‖ * C a) Filter.cofinite
            (nhds 0)

Defined in

Mathlib.RingTheory.MvPowerSeries.Restricted

Cited by

1 results in Mathlib

Foundations

Depth 157 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddMonoidFinset.HasAntidiagonalNormedRingIsUltrametricDist