QuaternionBasis

📁 Source: Mathlib/Algebra/QuaternionBasis.lean

Statistics

Metric	Count
Definitions `compHom`, `i`, `instInhabited`, `j`, `k`, `liftHom`, `self`	7
Theorems `hom_ext`, `hom_ext_iff`, `ext`, `ext_iff`, `i_compHom`, `i_mul_i`, `i_mul_j`, `i_mul_k`, `i_self`, `j_compHom`, `j_mul_i`, `j_mul_j`, `j_mul_k`, `j_self`, `k_compHom`, `k_mul_i`, `k_mul_j`, `k_mul_k`, `k_self`, `liftHom_apply`, `lift_add`, `lift_mul`, `lift_one`, `lift_smul`, `lift_zero`, `range_liftHom`, `hom_ext`, `hom_ext_iff`, `lift_apply`, `lift_symm_apply`	30
Total	37

Quaternion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_ext` 📖	—	`DFunLike.coe` `AlgHom` `Quaternion` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `algebra` `Algebra.id` `AlgHom.funLike` `QuaternionAlgebra.Basis.i` `QuaternionAlgebra` `QuaternionAlgebra.instRing` `QuaternionAlgebra.instAlgebra` `QuaternionAlgebra.Basis.self` `QuaternionAlgebra.Basis.j`	—	—	`QuaternionAlgebra.hom_ext`
`hom_ext_iff` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Quaternion` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `algebra` `Algebra.id` `AlgHom.funLike` `QuaternionAlgebra.Basis.i` `QuaternionAlgebra` `QuaternionAlgebra.instRing` `QuaternionAlgebra.instAlgebra` `QuaternionAlgebra.Basis.self` `QuaternionAlgebra.Basis.j`	—	`hom_ext`

QuaternionAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_ext` 📖	—	`DFunLike.coe` `AlgHom` `QuaternionAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `instAlgebra` `Algebra.id` `AlgHom.funLike` `Basis.i` `Basis.self` `Basis.j`	—	—	`Equiv.injective` `Basis.ext`
`hom_ext_iff` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `QuaternionAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `instAlgebra` `Algebra.id` `AlgHom.funLike` `Basis.i` `Basis.self` `Basis.j`	—	`hom_ext`
`lift_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Basis` `AlgHom` `QuaternionAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `instAlgebra` `Algebra.id` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `Basis.liftHom`	—	—
`lift_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AlgHom` `QuaternionAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `instAlgebra` `Algebra.id` `Basis` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lift` `Basis.compHom` `Basis.self`	—	—

QuaternionAlgebra.Basis

Definitions

Name	Category	Theorems
`compHom` 📖	CompOp	4 math math: `j_compHom`, `k_compHom`, `i_compHom`, `QuaternionAlgebra.lift_symm_apply`
`i` 📖	CompOp	14 math math: `i_mul_i`, `k_mul_i`, `i_mul_j`, `ext_iff`, `CliffordAlgebraQuaternion.i_quaternionBasis`, `j_mul_k`, `i_compHom`, `QuaternionAlgebra.hom_ext_iff`, `i_self`, `j_mul_i`, `range_liftHom`, `Quaternion.hom_ext_iff`, `k_mul_j`, `i_mul_k`
`instInhabited` 📖	CompOp	—
`j` 📖	CompOp	14 math math: `CliffordAlgebraQuaternion.j_quaternionBasis`, `k_mul_i`, `j_mul_j`, `i_mul_j`, `ext_iff`, `j_compHom`, `j_mul_k`, `QuaternionAlgebra.hom_ext_iff`, `j_self`, `j_mul_i`, `range_liftHom`, `Quaternion.hom_ext_iff`, `k_mul_j`, `i_mul_k`
`k` 📖	CompOp	11 math math: `k_mul_i`, `i_mul_j`, `CliffordAlgebraQuaternion.k_quaternionBasis`, `k_compHom`, `j_mul_k`, `k_self`, `k_mul_k`, `j_mul_i`, `range_liftHom`, `k_mul_j`, `i_mul_k`
`liftHom` 📖	CompOp	3 math math: `QuaternionAlgebra.lift_apply`, `liftHom_apply`, `range_liftHom`
`self` 📖	CompOp	6 math math: `k_self`, `QuaternionAlgebra.lift_symm_apply`, `QuaternionAlgebra.hom_ext_iff`, `i_self`, `j_self`, `Quaternion.hom_ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`i` `j`	—	—	—
`ext_iff` 📖	mathematical	—	`i` `j`	—	`ext`
`i_compHom` 📖	mathematical	—	`i` `compHom` `DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `Ring.toSemiring` `AlgHom.funLike`	—	—
`i_mul_i` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `i` `Distrib.toAdd` `Algebra.toSMul` `CommRing.toCommSemiring` `Ring.toSemiring` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	—
`i_mul_j` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `i` `j` `k`	—	—
`i_mul_k` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `i` `k` `Distrib.toAdd` `Algebra.toSMul` `CommRing.toCommSemiring` `Ring.toSemiring` `j`	—	`i_mul_j` `mul_assoc` `i_mul_i` `add_mul` `Distrib.rightDistribClass` `smul_mul_assoc` `IsScalarTower.right` `one_mul`
`i_self` 📖	mathematical	—	`i` `QuaternionAlgebra` `QuaternionAlgebra.instRing` `QuaternionAlgebra.instAlgebra` `CommRing.toCommSemiring` `Algebra.id` `self` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—
`j_compHom` 📖	mathematical	—	`j` `compHom` `DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `Ring.toSemiring` `AlgHom.funLike`	—	—
`j_mul_i` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `j` `i` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Algebra.toSMul` `CommRing.toCommSemiring` `Ring.toSemiring` `k`	—	—
`j_mul_j` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `j` `Algebra.toSMul` `CommRing.toCommSemiring` `Ring.toSemiring` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	—
`j_mul_k` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `j` `k` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Algebra.toSMul` `CommRing.toCommSemiring` `Ring.toSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `i`	—	`i_mul_j` `mul_assoc` `j_mul_i` `sub_mul` `smul_mul_assoc` `IsScalarTower.right` `j_mul_j` `smul_assoc` `IsScalarTower.left` `k_mul_j`
`j_self` 📖	mathematical	—	`j` `QuaternionAlgebra` `QuaternionAlgebra.instRing` `QuaternionAlgebra.instAlgebra` `CommRing.toCommSemiring` `Algebra.id` `self` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—
`k_compHom` 📖	mathematical	—	`k` `compHom` `DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `Ring.toSemiring` `AlgHom.funLike`	—	—
`k_mul_i` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `k` `i` `Algebra.toSMul` `CommRing.toCommSemiring` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `j`	—	`i_mul_j` `mul_assoc` `j_mul_i` `mul_sub` `i_mul_k` `neg_smul` `mul_smul_comm` `Algebra.to_smulCommClass` `Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `Mathlib.Tactic.LinearCombination.eq_rearrange` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.add_eq_eval₃` `add_zero` `Mathlib.Tactic.Module.NF.sub_eq_eval₂` `Mathlib.Tactic.Module.NF.zero_sub_eq_eval` `Mathlib.Tactic.Module.NF.zero_eq_eval` `Mathlib.Tactic.Module.NF.neg_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval₁` `Mathlib.Tactic.Module.NF.eq_cons_const` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Meta.NormNum.IsNat.to_raw_eq`
`k_mul_j` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `k` `j` `Algebra.toSMul` `CommRing.toCommSemiring` `Ring.toSemiring` `i`	—	`i_mul_j` `mul_assoc` `j_mul_j` `mul_smul_comm` `Algebra.to_smulCommClass` `mul_one`
`k_mul_k` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `k` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Algebra.toSMul` `CommRing.toCommSemiring` `Ring.toSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`i_mul_j` `mul_assoc` `j_mul_i` `mul_sub` `i_mul_i` `add_mul` `Distrib.rightDistribClass` `smul_mul_assoc` `IsScalarTower.right` `one_mul` `sub_mul` `mul_smul_comm` `Algebra.to_smulCommClass` `j_mul_j` `smul_smul` `Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `Mathlib.Tactic.LinearCombination.eq_rearrange` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.add_eq_eval₃` `add_zero` `Mathlib.Tactic.Module.NF.sub_eq_eval₂` `Mathlib.Tactic.Module.NF.zero_sub_eq_eval` `Mathlib.Tactic.Module.NF.zero_eq_eval` `Mathlib.Tactic.Module.NF.neg_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval₁` `Mathlib.Tactic.Module.NF.eq_cons_const` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Meta.NormNum.IsNat.to_raw_eq`
`k_self` 📖	mathematical	—	`k` `QuaternionAlgebra` `QuaternionAlgebra.instRing` `QuaternionAlgebra.instAlgebra` `CommRing.toCommSemiring` `Algebra.id` `self` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—
`liftHom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `QuaternionAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `QuaternionAlgebra.instRing` `QuaternionAlgebra.instAlgebra` `Algebra.id` `AlgHom.funLike` `liftHom` `lift`	—	—
`lift_add` 📖	mathematical	—	`lift` `QuaternionAlgebra` `QuaternionAlgebra.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `add_smul` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg`
`lift_mul` 📖	mathematical	—	`lift` `QuaternionAlgebra` `QuaternionAlgebra.instMul` `CommRing.toRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Algebra.algebraMap_eq_smul_one` `add_mul` `Distrib.rightDistribClass` `mul_add` `Distrib.leftDistribClass` `smul_mul_assoc` `IsScalarTower.right` `mul_smul_comm` `Algebra.to_smulCommClass` `one_mul` `mul_one` `smul_smul` `i_mul_i` `i_mul_j` `i_mul_k` `j_mul_i` `j_mul_j` `j_mul_k` `k_mul_i` `k_mul_j` `k_mul_k` `sub_eq_add_neg` `neg_smul` `smul_neg` `mul_right_comm` `mul_comm` `add_smul` `Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `Mathlib.Tactic.LinearCombination.eq_rearrange` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.add_eq_eval₂` `zero_add` `Mathlib.Tactic.Module.NF.neg_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval₁` `Mathlib.Tactic.Module.NF.zero_eq_eval` `add_zero` `AddCommGroup.intIsScalarTower` `Mathlib.Tactic.Module.NF.sub_eq_eval₂` `Mathlib.Tactic.Module.NF.zero_sub_eq_eval` `Mathlib.Tactic.Module.NF.eq_cons_const` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `eq_intCast` `Int.cast_neg` `Int.cast_one`
`lift_one` 📖	mathematical	—	`lift` `QuaternionAlgebra` `QuaternionAlgebra.instOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `zero_smul` `add_zero`
`lift_smul` 📖	mathematical	—	`lift` `QuaternionAlgebra` `QuaternionAlgebra.instSMul` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Ring.toSemiring`	—	`map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `SemigroupAction.mul_smul` `smul_add`
`lift_zero` 📖	mathematical	—	`lift` `QuaternionAlgebra` `QuaternionAlgebra.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `zero_smul` `add_zero`
`range_liftHom` 📖	mathematical	—	`AlgHom.range` `QuaternionAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `QuaternionAlgebra.instRing` `QuaternionAlgebra.instAlgebra` `Algebra.id` `liftHom` `Algebra.adjoin` `Set` `Set.instInsert` `i` `j` `Set.instSingletonSet` `k`	—	`le_antisymm` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `SubsemiringClass.toAddSubmonoidClass` `Subalgebra.instSubsemiringClass` `algebraMap_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `Subalgebra.instSMulMemClass` `Subalgebra.smul_mem` `Algebra.subset_adjoin` `Algebra.adjoin_le_iff` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_smul` `zero_add` `zero_smul` `add_zero`

---

← Back to Index