Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-04 05:43 7ab3ca85

View on Github →

feat(data/quaternion): define quaternions and prove some basic properties (#2339)

Estimated changes

Modified src/algebra/algebra/basic.lean

added theorem opposite.algebra_map_apply

added theorem opposite.op_smul

Modified src/algebra/big_operators/basic.lean

added theorem finset.op_sum

added theorem finset.unop_sum

Modified src/algebra/big_operators/order.lean

deleted theorem with_top.op_sum

deleted theorem with_top.unop_sum

Modified src/algebra/module/linear_map.lean

added theorem linear_equiv.coe_of_involutive

added def linear_equiv.of_involutive

Modified src/algebra/opposites.lean

added theorem opposite.coe_op_add_equiv

added theorem opposite.coe_op_add_equiv_symm

deleted theorem opposite.coe_op_add_hom

deleted theorem opposite.coe_unop_add_hom

added def opposite.op_add_equiv

added theorem opposite.op_add_equiv_to_equiv

deleted def opposite.op_add_hom

deleted def opposite.unop_add_hom

added theorem ring_hom.coe_to_opposite

added def ring_hom.to_opposite

Modified src/analysis/normed_space/inner_product.lean

Created src/analysis/quaternion.lean

added theorem quaternion.coe_complex_add

added theorem quaternion.coe_complex_coe

added theorem quaternion.coe_complex_im_i

added theorem quaternion.coe_complex_im_j

added theorem quaternion.coe_complex_im_k

added theorem quaternion.coe_complex_mul

added theorem quaternion.coe_complex_one

added theorem quaternion.coe_complex_re

added theorem quaternion.coe_complex_smul

added theorem quaternion.coe_complex_zero

added theorem quaternion.coe_of_complex

added theorem quaternion.inner_def

added theorem quaternion.inner_self

added theorem quaternion.norm_coe

added theorem quaternion.norm_mul

added theorem quaternion.norm_sq_eq_norm_square

added def quaternion.of_complex

Created src/data/quaternion.lean

added theorem quaternion.add_im_i

added theorem quaternion.add_im_j

added theorem quaternion.add_im_k

added theorem quaternion.add_re

added theorem quaternion.algebra_map_def

added theorem quaternion.coe_add

added theorem quaternion.coe_commute

added theorem quaternion.coe_commutes

added theorem quaternion.coe_conj_alg_equiv

added theorem quaternion.coe_im_i

added theorem quaternion.coe_im_j

added theorem quaternion.coe_im_k

added theorem quaternion.coe_inj

added theorem quaternion.coe_injective

added theorem quaternion.coe_mul

added theorem quaternion.coe_mul_eq_smul

added theorem quaternion.coe_neg

added theorem quaternion.coe_norm_sq_add

added theorem quaternion.coe_one

added theorem quaternion.coe_re

added theorem quaternion.coe_sub

added theorem quaternion.coe_zero

added theorem quaternion.commute_conj_conj

added theorem quaternion.commute_conj_self

added theorem quaternion.commute_self_conj

added def quaternion.conj

added theorem quaternion.conj_add

added theorem quaternion.conj_add_self'

added theorem quaternion.conj_add_self

added def quaternion.conj_alg_equiv

added theorem quaternion.conj_coe

added theorem quaternion.conj_conj

added theorem quaternion.conj_conj_mul

added theorem quaternion.conj_eq_two_re_sub

added theorem quaternion.conj_fixed

added theorem quaternion.conj_im_i

added theorem quaternion.conj_im_j

added theorem quaternion.conj_im_k

added theorem quaternion.conj_mul

added theorem quaternion.conj_mul_conj

added theorem quaternion.conj_mul_eq_coe

added theorem quaternion.conj_mul_self

added theorem quaternion.conj_neg

added theorem quaternion.conj_one

added theorem quaternion.conj_re

added theorem quaternion.conj_smul

added theorem quaternion.conj_sub

added theorem quaternion.conj_zero

added theorem quaternion.eq_re_iff_mem_range_coe

added theorem quaternion.eq_re_of_eq_coe

added theorem quaternion.ext

added theorem quaternion.ext_iff

added theorem quaternion.mul_coe_eq_smul

added theorem quaternion.mul_conj_eq_coe

added theorem quaternion.mul_im_i

added theorem quaternion.mul_im_j

added theorem quaternion.mul_im_k

added theorem quaternion.mul_re

added theorem quaternion.neg_im_i

added theorem quaternion.neg_im_j

added theorem quaternion.neg_im_k

added theorem quaternion.neg_re

added def quaternion.norm_sq

added theorem quaternion.norm_sq_coe

added theorem quaternion.norm_sq_def'

added theorem quaternion.norm_sq_def

added theorem quaternion.norm_sq_div

added theorem quaternion.norm_sq_eq_zero

added theorem quaternion.norm_sq_inv

added theorem quaternion.norm_sq_le_zero

added theorem quaternion.norm_sq_ne_zero

added theorem quaternion.norm_sq_neg

added theorem quaternion.norm_sq_nonneg

added theorem quaternion.norm_sq_zero

added theorem quaternion.one_im_i

added theorem quaternion.one_im_j

added theorem quaternion.one_im_k

added theorem quaternion.one_re

added theorem quaternion.self_add_conj'

added theorem quaternion.self_add_conj

added theorem quaternion.self_mul_conj

added theorem quaternion.smul_coe

added theorem quaternion.smul_im_i

added theorem quaternion.smul_im_j

added theorem quaternion.smul_im_k

added theorem quaternion.smul_re

added theorem quaternion.sub_im_i

added theorem quaternion.sub_im_j

added theorem quaternion.sub_im_k

added theorem quaternion.sub_re

added theorem quaternion.zero_im_i

added theorem quaternion.zero_im_j

added theorem quaternion.zero_im_k

added theorem quaternion.zero_re

added def quaternion

added theorem quaternion_algebra.coe_add

added theorem quaternion_algebra.coe_algebra_map

added theorem quaternion_algebra.coe_commute

added theorem quaternion_algebra.coe_commutes

added theorem quaternion_algebra.coe_conj_alg_equiv

added theorem quaternion_algebra.coe_im_i

added theorem quaternion_algebra.coe_im_j

added theorem quaternion_algebra.coe_im_k

added theorem quaternion_algebra.coe_inj

added theorem quaternion_algebra.coe_injective

added theorem quaternion_algebra.coe_mul

added theorem quaternion_algebra.coe_mul_eq_smul

added theorem quaternion_algebra.coe_neg

added theorem quaternion_algebra.coe_one

added theorem quaternion_algebra.coe_re

added theorem quaternion_algebra.coe_sub

added theorem quaternion_algebra.coe_zero

added theorem quaternion_algebra.commute_conj_conj

added theorem quaternion_algebra.commute_conj_self

added theorem quaternion_algebra.commute_self_conj

added def quaternion_algebra.conj

added theorem quaternion_algebra.conj_add

added theorem quaternion_algebra.conj_add_self'

added theorem quaternion_algebra.conj_add_self

added def quaternion_algebra.conj_alg_equiv

added theorem quaternion_algebra.conj_coe

added theorem quaternion_algebra.conj_conj

added theorem quaternion_algebra.conj_conj_mul

added theorem quaternion_algebra.conj_eq_two_re_sub

added theorem quaternion_algebra.conj_fixed

added theorem quaternion_algebra.conj_mul

added theorem quaternion_algebra.conj_mul_conj

added theorem quaternion_algebra.conj_mul_eq_coe

added theorem quaternion_algebra.conj_neg

added theorem quaternion_algebra.conj_one

added theorem quaternion_algebra.conj_smul

added theorem quaternion_algebra.conj_sub

added theorem quaternion_algebra.conj_zero

added theorem quaternion_algebra.eq_re_iff_mem_range_coe

added theorem quaternion_algebra.eq_re_of_eq_coe

added theorem quaternion_algebra.im_i_conj

added theorem quaternion_algebra.im_j_conj

added theorem quaternion_algebra.im_k_conj

added theorem quaternion_algebra.mk.eta

added theorem quaternion_algebra.mk_add_mk

added theorem quaternion_algebra.mk_mul_mk

added theorem quaternion_algebra.mk_sub_mk

added theorem quaternion_algebra.mul_coe_eq_smul

added theorem quaternion_algebra.mul_conj_eq_coe

added theorem quaternion_algebra.neg_mk

added theorem quaternion_algebra.re_conj

added theorem quaternion_algebra.self_add_conj'

added theorem quaternion_algebra.self_add_conj

added theorem quaternion_algebra.smul_coe

added theorem quaternion_algebra.smul_im_i

added theorem quaternion_algebra.smul_im_j

added theorem quaternion_algebra.smul_im_k

added theorem quaternion_algebra.smul_re

added structure quaternion_algebra

Modified src/number_theory/arithmetic_function.lean