Theorems · Theorem · linear algebra

MultilinearMap.ext_ring

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

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

Defined in

Mathlib.LinearAlgebra.Multilinear.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleFinite