English
The quaternion algebra ℍ[R] is a division ring extending the field structure of R.
Русский
Кватернионная алгебра ℍ[R] образует деление-кольцо, расширяющее поля R.
LaTeX
$$DivisionRing (ℍ[R]) extending Field R$$
Lean4
instance instDivisionRing : DivisionRing ℍ[R]
where
__ := Quaternion.instRing
__ := Quaternion.instGroupWithZero
nnqsmul := (· • ·)
qsmul := (· • ·)
nnratCast_def _ := by rw [← coe_nnratCast, NNRat.cast_def, coe_div, coe_natCast, coe_natCast]
ratCast_def _ := by rw [← coe_ratCast, Rat.cast_def, coe_div, coe_intCast, coe_natCast]
nnqsmul_def _ _ := by rw [← coe_nnratCast, coe_mul_eq_smul]; ext <;> exact NNRat.smul_def ..
qsmul_def _ _ := by rw [← coe_ratCast, coe_mul_eq_smul]; ext <;> exact Rat.smul_def ..
