Commit 2023-02-09 15:58 24f7dbdf

View on Github →

feat(analysis/quaternion): add complete_space, module.free, and module.finite instances (#18347) The main trick here is showing that the quaternions are in isometric equivalence with 4D euclidean space.

Estimated changes

Modified src/algebra/quaternion.lean

added theorem quaternion.dim_eq_four

added def quaternion.equiv_tuple

added theorem quaternion.equiv_tuple_apply

added theorem quaternion.finrank_eq_four

added theorem quaternion_algebra.coe_basis_one_i_j_k_repr

added theorem quaternion_algebra.coe_linear_equiv_tuple

added theorem quaternion_algebra.coe_linear_equiv_tuple_symm

added theorem quaternion_algebra.dim_eq_four

added def quaternion_algebra.equiv_tuple

added theorem quaternion_algebra.equiv_tuple_apply

added theorem quaternion_algebra.finrank_eq_four

added def quaternion_algebra.linear_equiv_tuple

Modified src/analysis/quaternion.lean

added theorem quaternion.continuous_im_i

added theorem quaternion.continuous_im_j

added theorem quaternion.continuous_im_k

added theorem quaternion.continuous_re

added theorem quaternion.norm_pi_Lp_equiv_symm_equiv_tuple