Theorems · Theorem · number theory

QuadraticMap.polar_add_left_iff

∀ {M : Type u_4} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {f : M → N} {x x' y : M},
  QuadraticMap.polar f (x + x') y = QuadraticMap.polar f x y + QuadraticMap.polar f x' y ↔
    f (x + x' + y) + (f x + f x' + f y) = f (x + x') + f (x' + y) + f (y + x)

Auxiliary lemma to express bilinearity of QuadraticMap.polar without subtraction.

Defined in

Mathlib.LinearAlgebra.QuadraticForm.Basic

Cited by

1 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext

Assumes

AddCommGroupAddCommGroup