Commit 2023-02-10 12:21 d3e3adc9

View on Github →

chore(algebra/quaternion): missing trivial lemmas (#18413) A mixture of trivial algebraic results and trivial topological ones. This also changes the rat.cast instance on quaternions to be slightly nicer.

Estimated changes

Modified src/algebra/quaternion.lean

added theorem quaternion.coe_div

added theorem quaternion.coe_int_cast

added theorem quaternion.coe_inv

added theorem quaternion.coe_nat_cast

added theorem quaternion.coe_pow

added theorem quaternion.coe_rat_cast

added theorem quaternion.coe_zpow

modified theorem quaternion.conj_coe

added theorem quaternion.conj_int_cast

added theorem quaternion.conj_inv

added theorem quaternion.conj_nat_cast

added theorem quaternion.conj_pow

added theorem quaternion.conj_rat_cast

added theorem quaternion.conj_zpow

added theorem quaternion.int_cast_im_i

added theorem quaternion.int_cast_im_j

added theorem quaternion.int_cast_im_k

added theorem quaternion.int_cast_re

added theorem quaternion.nat_cast_im_i

added theorem quaternion.nat_cast_im_j

added theorem quaternion.nat_cast_im_k

added theorem quaternion.nat_cast_re

added theorem quaternion.norm_sq_conj

added theorem quaternion.norm_sq_int_cast

added theorem quaternion.norm_sq_nat_cast

added theorem quaternion.norm_sq_rat_cast

added theorem quaternion.norm_sq_zpow

added theorem quaternion.rat_cast_im_i

added theorem quaternion.rat_cast_im_j

added theorem quaternion.rat_cast_im_k

added theorem quaternion.rat_cast_re

added theorem quaternion_algebra.coe_int_cast

added theorem quaternion_algebra.coe_nat_cast

added theorem quaternion_algebra.coe_pow

modified theorem quaternion_algebra.conj_coe

added theorem quaternion_algebra.conj_int_cast

added theorem quaternion_algebra.conj_nat_cast

added theorem quaternion_algebra.conj_pow

added theorem quaternion_algebra.int_cast_im_i

added theorem quaternion_algebra.int_cast_im_j

added theorem quaternion_algebra.int_cast_im_k

added theorem quaternion_algebra.int_cast_re

added theorem quaternion_algebra.nat_cast_im_i

added theorem quaternion_algebra.nat_cast_im_j

added theorem quaternion_algebra.nat_cast_im_k

added theorem quaternion_algebra.nat_cast_re

Modified src/analysis/quaternion.lean

added theorem quaternion.continuous_coe

added theorem quaternion.continuous_conj

added theorem quaternion.continuous_norm_sq

added theorem quaternion.nnnorm_conj

added theorem quaternion.norm_conj