English
Define dualProd as the quadratic form on the product (Module.Dual R M × M) by Q(f, x) = f(x). This is the natural pairing between the dual and the primal module.
Русский
Определим dualProd как квадратичную форму на произведении (Module.Dual R M × M) по формуле Q(f,x) = f(x). Это естественное парирование между дуальным и исходным модулем.
LaTeX
$$$ dualProd: (f,x) \\mapsto f(x) $$$
Lean4
/-- The quadratic form on `Module.Dual R M × M` defined as `Q (f, x) = f x`. -/
@[simps]
def dualProd : QuadraticForm R (Module.Dual R M × M)
where
toFun p := p.1 p.2
toFun_smul a
p := by
rw [Prod.smul_fst, Prod.smul_snd, LinearMap.smul_apply, LinearMap.map_smul, smul_eq_mul, smul_eq_mul, smul_eq_mul,
mul_assoc]
exists_companion' :=
⟨LinearMap.dualProd R M, fun p q => by
rw [LinearMap.dualProd_apply_apply, Prod.fst_add, Prod.snd_add, LinearMap.add_apply, map_add, map_add,
add_right_comm _ (q.1 q.2), add_comm (q.1 p.2) (p.1 q.2), ← add_assoc, ← add_assoc]⟩
