Theorems · Definition · number theory

QuadraticMap.IsometryEquiv.pi

{ι : Type u_1} →
  {R : Type u_2} →
    {P : Type u_7} →
      {Mᵢ : ι → Type u_8} →
        {Nᵢ : ι → Type u_9} →
          [inst : CommSemiring R] →
            [inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)] →
              [inst_2 : (i : ι) → AddCommMonoid (Nᵢ i)] →
                [inst_3 : AddCommMonoid P] →
                  [inst_4 : (i : ι) → Module R (Mᵢ i)] →
                    [inst_5 : (i : ι) → Module R (Nᵢ i)] →
                      [inst_6 : Module R P] →
                        [inst_7 : Fintype ι] →
                          {Q : (i : ι) → QuadraticMap R (Mᵢ i) P} →
                            {Q' : (i : ι) → QuadraticMap R (Nᵢ i) P} →
                              ((i : ι) → (Q i).IsometryEquiv (Q' i)) →
                                (QuadraticMap.pi Q).IsometryEquiv (QuadraticMap.pi Q')

An isometry between quadratic forms generated by QuadraticMap.pi can be constructed from a pair of isometries between the left and right parts.

Defined in

Mathlib.LinearAlgebra.QuadraticForm.Prod

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModuleFintype