Theorems · Definition · number theory

QuadraticMap.Isometry.proj

{ι : Type u_1} →
  {R : Type u_2} →
    {P : Type u_7} →
      {Mᵢ : ι → Type u_8} →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)] →
            [inst_2 : AddCommMonoid P] →
              [inst_3 : (i : ι) → Module R (Mᵢ i)] →
                [inst_4 : Module R P] →
                  [inst_5 : Fintype ι] →
                    [inst_6 : DecidableEq ι] →
                      (i : ι) → (Q : QuadraticMap R (Mᵢ i) P) → QuadraticMap.pi (Pi.single i Q) →qᵢ Q

LinearMap.proj as an isometry, when all but one quadratic form is zero.

Defined in

Mathlib.LinearAlgebra.QuadraticForm.Prod

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidAddCommMonoidModuleModuleFintypeDecidableEq