[Merged by Bors] - chore(Mathlib/Algebra/Quaternion): Generalize Quaternion Algebra

[Whysoserioushah]

---

[github-actions]

PR summary 02b578ab07

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ coe_ofNat
+ comm
+ instance : Add ℍ[R,c₁,c₂,c₃]
+ instance : AddCommGroupWithOne ℍ[R,c₁,c₂,c₃]
+ instance : CoeTC R ℍ[R,c₁,c₂,c₃] := ⟨coe⟩
+ instance : Inhabited (Basis ℍ[R,c₁,c₂,c₃] c₁ c₂ c₃)
+ instance : Inhabited ℍ[R,c₁,c₂,c₃] := ⟨0⟩
+ instance : Inhabited ℍ[R] := inferInstanceAs <| Inhabited ℍ[R,-1, 0, -1]
+ instance : IsStarNormal a := inferInstanceAs <| IsStarNormal (R := ℍ[R,-1,0,-1]) a
+ instance : Module.Finite R ℍ[R,c₁,c₂,c₃] := .of_basis (basisOneIJK c₁ c₂ c₃)
+ instance : Module.Finite R ℍ[R] := inferInstanceAs <| Module.Finite R ℍ[R,-1,0,-1]
+ instance : Module.Free R ℍ[R,c₁,c₂,c₃] := .of_basis (basisOneIJK c₁ c₂ c₃)
+ instance : Module.Free R ℍ[R] := inferInstanceAs <| Module.Free R ℍ[R,-1,0,-1]
+ instance : Mul ℍ[R,c₁,c₂,c₃]
+ instance : Neg ℍ[R,c₁,c₂,c₃] := ⟨fun a => ⟨-a.1, -a.2, -a.3, -a.4⟩⟩
+ instance : One ℍ[R,c₁,c₂,c₃] := ⟨⟨1, 0, 0, 0⟩⟩
+ instance : SMul S ℍ[R,c₁,c₂,c₃] where smul s a := ⟨s • a.1, s • a.2, s • a.3, s • a.4⟩
+ instance : Sub ℍ[R,c₁,c₂,c₃]
+ instance : Zero ℍ[R,c₁,c₂,c₃] := ⟨⟨0, 0, 0, 0⟩⟩
+ instance [AddCommGroup R] : AddCommGroup ℍ[R,c₁,c₂,c₃]
+ instance [CommSemiring S] [Algebra S R] : Algebra S ℍ[R,c₁,c₂,c₃]
+ instance [NoZeroDivisors R] : NoZeroSMulDivisors R ℍ[R,c₁,c₂,c₃] := ⟨by
+ instance [Nontrivial R] : Nontrivial ℍ[R, c₁, c₂, c₃] := (equivTuple c₁ c₂ c₃).surjective.nontrivial
+ instance [Repr R] {a b c : R} : Repr ℍ[R, a, b, c]
+ instance [SMul S R] : SMul S ℍ[R] := inferInstanceAs <| SMul S ℍ[R,-1, 0, -1]
+ instance [SMul S T] [IsScalarTower S T R] : IsScalarTower S T ℍ[R,c₁,c₂,c₃]
+ instance [SMulCommClass S T R] : SMulCommClass S T ℍ[R,c₁,c₂,c₃]
+ instance [Subsingleton R] : Subsingleton ℍ[R, c₁, c₂, c₃] := (equivTuple c₁ c₂ c₃).subsingleton
+ instance {R : Type*} [Zero R] [One R] [Neg R] [Nontrivial R] : Nontrivial ℍ[R]
+ instance {R : Type*} [Zero R] [One R] [Neg R] [Subsingleton R] : Subsingleton ℍ[R]
+ ofNat_im
+ ofNat_imI
+ ofNat_imJ
+ ofNat_imK
+ ofNat_re
+ star_smul'
++-- star_eq_two_re_sub
+-+- lift
+-+- self_add_star
+-+- self_add_star'
+-+- star_add_self
+-+- star_add_self'
- instance : Add ℍ[R,c₁,c₂]
- instance : AddCommGroupWithOne ℍ[R,c₁,c₂]
- instance : CoeTC R ℍ[R,c₁,c₂] := ⟨coe⟩
- instance : Inhabited (Basis ℍ[R,c₁,c₂] c₁ c₂)
- instance : Inhabited ℍ[R,c₁,c₂] := ⟨0⟩
- instance : Inhabited ℍ[R] := inferInstanceAs <| Inhabited ℍ[R,-1,-1]
- instance : IsStarNormal a := inferInstanceAs <| IsStarNormal (R := ℍ[R,-1,-1]) a
- instance : Module.Finite R ℍ[R,c₁,c₂] := .of_basis (basisOneIJK c₁ c₂)
- instance : Module.Finite R ℍ[R] := inferInstanceAs <| Module.Finite R ℍ[R,-1,-1]
- instance : Module.Free R ℍ[R,c₁,c₂] := .of_basis (basisOneIJK c₁ c₂)
- instance : Module.Free R ℍ[R] := inferInstanceAs <| Module.Free R ℍ[R,-1,-1]
- instance : Mul ℍ[R,c₁,c₂]
- instance : Neg ℍ[R,c₁,c₂] := ⟨fun a => ⟨-a.1, -a.2, -a.3, -a.4⟩⟩
- instance : One ℍ[R,c₁,c₂] := ⟨⟨1, 0, 0, 0⟩⟩
- instance : SMul S ℍ[R,c₁,c₂] where smul s a := ⟨s • a.1, s • a.2, s • a.3, s • a.4⟩
- instance : Sub ℍ[R,c₁,c₂]
- instance : Zero ℍ[R,c₁,c₂] := ⟨⟨0, 0, 0, 0⟩⟩
- instance [AddCommGroup R] : AddCommGroup ℍ[R,c₁,c₂]
- instance [CommSemiring S] [Algebra S R] : Algebra S ℍ[R,c₁,c₂]
- instance [NoZeroDivisors R] : NoZeroSMulDivisors R ℍ[R,c₁,c₂] := ⟨by
- instance [Nontrivial R] : Nontrivial ℍ[R, c₁, c₂] := (equivTuple c₁ c₂).surjective.nontrivial
- instance [Repr R] {a b : R} : Repr ℍ[R, a, b]
- instance [SMul S R] : SMul S ℍ[R] := inferInstanceAs <| SMul S ℍ[R,-1,-1]
- instance [SMul S T] [IsScalarTower S T R] : IsScalarTower S T ℍ[R,c₁,c₂]
- instance [SMulCommClass S T R] : SMulCommClass S T ℍ[R,c₁,c₂]
- instance [Subsingleton R] : Subsingleton ℍ[R, c₁, c₂] := (equivTuple c₁ c₂).subsingleton
- instance {R : Type*} [One R] [Neg R] [Nontrivial R] : Nontrivial ℍ[R]
- instance {R : Type*} [One R] [Neg R] [Subsingleton R] : Subsingleton ℍ[R]

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[kbuzzard]

This looks fine to me. I've left a bunch of comments, mostly superficial. I'm reluctant to merge this myself because you're my Masters student...

[Whysoserioushah]

Now I think maybe the PR is ready?

[mathlib-bors]

✌️ kbuzzard can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[kbuzzard]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style