Theorems · Theorem · functional analysis

ContinuousMultilinearMap.ext_ring

∀ {R : Type u} {ι : Type v} {M₂ : Type w₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  [inst_3 : TopologicalSpace M₂] [Finite ι] [inst_5 : TopologicalSpace R]
  ⦃f g : ContinuousMultilinearMap R (fun x => R) M₂⦄, ((f fun x => 1) = g fun x => 1) → f = g

If two continuous R-multilinear maps from R are equal on 1, then they are equal. This is the multilinear version of ContinuousLinearMap.ext_ring.

Defined in

Mathlib.Topology.Algebra.Module.Multilinear.Basic

Cited by

20 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleTopologicalSpaceFiniteTopologicalSpace