Mathlib Map

Theorems · Theorem · several complex variables

analyticAt_mul

∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {A : Type u_7} [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  (z : A × A), AnalyticAt 𝕜 (fun x => x.1 * x.2) z

Multiplication in a normed algebra over 𝕜 is analytic.

Defined in
Mathlib.Analysis.Analytic.Constructions
Cited by
1 results in Mathlib
Foundations
Depth 187 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NontriviallyNormedFieldNormedRingNormedAlgebra
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AnalyticWithinAt.mul · cited by 5AnalyticWithinAt.mulNontriviallyNormedField · cited by 8742NontriviallyNormedFieldNormedAlgebra · cited by 1165NormedAlgebraNormedRing · cited by 924NormedRingAnalyticAt · cited by 321AnalyticAtanalyticAt_smul · cited by 3analyticAt_smulanalyticAt_mulCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.