IntUnitsPower

📁 Source: Mathlib/Data/ZMod/IntUnitsPower.lean

Statistics

Metric	Count
Definitions instUnitsPow, instModuleZModOfNatNatAdditiveUnitsInt, instSMulZModOfNatNatAdditiveUnitsInt	3
Theorems natCast_smul_units, smul_units_def, mul_uzpow, ofMul_uzpow, one_uzpow, toMul_uzpow, uzpow_add, uzpow_coe_nat, uzpow_intCast, uzpow_mul, uzpow_natCast, uzpow_neg, uzpow_one, uzpow_sub, uzpow_zero	15
Total	18

Int

Definitions

Name	Category	Theorems
instUnitsPow 📖	CompOp	24 math math: ComplexShape.eulerCharSignsDownNat_χ, toMul_uzpow, uzpow_zero, uzpow_natCast, uzpow_coe_nat, uzpow_one, GradedTensorProduct.tmul_coe_mul_coe_tmul, uzpow_mul, ComplexShape.ε_down_ℕ, CliffordAlgebra.map_mul_map_of_isOrtho_of_mem_evenOdd, NumberField.InfinitePlace.ComplexEmbedding.conjugate_sign, negOnePow_def, uzpow_add, one_uzpow, ComplexShape.eulerCharSignsUpNat_χ, GradedTensorProduct.comm_coe_tmul_coe, uzpow_sub, TensorProduct.tmul_of_gradedMul_of_tmul, uzpow_intCast, uzpow_neg, TensorProduct.gradedCommAux_lof_tmul, mul_uzpow, TensorProduct.gradedComm_of_tmul_of, ofMul_uzpow

ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natCast_smul_units 📖	mathematical	—	ZMod Additive Units Int.instMonoid instSMulZModOfNatNatAdditiveUnitsInt AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing commRing AddMonoid.toNatSMul Additive.addMonoid Units.instMonoid	—	Int.units_pow_eq_pow_mod_two
smul_units_def 📖	mathematical	—	ZMod Additive Units Int.instMonoid instSMulZModOfNatNatAdditiveUnitsInt AddMonoid.toNatSMul Additive.addMonoid Units.instMonoid val	—	—

(root)

Definitions

Name	Category	Theorems
instModuleZModOfNatNatAdditiveUnitsInt 📖	CompOp	8 math math: CliffordAlgebra.toProd_comp_ofProd, CliffordAlgebra.toProd_ι_tmul_one, CliffordAlgebra.map_mul_map_of_isOrtho_of_mem_evenOdd, CliffordAlgebra.prodEquiv_symm_apply, CliffordAlgebra.prodEquiv_apply, CliffordAlgebra.ofProd_comp_toProd, CliffordAlgebra.toProd_one_tmul_ι, CliffordAlgebra.ofProd_ι_mk
instSMulZModOfNatNatAdditiveUnitsInt 📖	CompOp	2 math math: ZMod.natCast_smul_units, ZMod.smul_units_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_uzpow 📖	mathematical	—	Units Int.instMonoid Int.instUnitsPow Units.instMul	—	Equiv.injective smul_add
ofMul_uzpow 📖	mathematical	—	DFunLike.coe Equiv Units Int.instMonoid Additive EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul Int.instUnitsPow SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero Additive.addZeroClass Units.instMulOneClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Additive.addMonoid Units.instMonoid Module.toDistribMulAction Additive.addCommMonoid CommGroup.toCommMonoid Units.instCommGroupUnits Int.instCommMonoid	—	—
one_uzpow 📖	mathematical	—	Units Int.instMonoid Int.instUnitsPow Units.instOne	—	Equiv.injective smul_zero
toMul_uzpow 📖	mathematical	—	DFunLike.coe Equiv Additive Units Int.instMonoid EquivLike.toFunLike Equiv.instEquivLike Additive.toMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero Additive.addZeroClass Units.instMulOneClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Additive.addMonoid Units.instMonoid Module.toDistribMulAction Additive.addCommMonoid CommGroup.toCommMonoid Units.instCommGroupUnits Int.instCommMonoid Int.instUnitsPow	—	—
uzpow_add 📖	mathematical	—	Units Int.instMonoid Int.instUnitsPow Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Units.instMul	—	Equiv.injective add_smul
uzpow_coe_nat 📖	mathematical	—	Units Int.instMonoid Int.instUnitsPow Nat.instCommSemiring AddCommMonoid.toNatModule Additive Additive.addCommMonoid CommGroup.toCommMonoid Units.instCommGroupUnits Int.instCommMonoid	—	uzpow_natCast
uzpow_intCast 📖	mathematical	—	Units Int.instMonoid Int.instUnitsPow CommRing.toCommSemiring AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing Int.instCommSemiring AddCommGroup.toIntModule Additive Additive.addCommGroup Units.instCommGroupUnits Int.instCommMonoid	—	Int.cast_smul_eq_zsmul toMul_zsmul toMul_ofMul
uzpow_mul 📖	mathematical	—	Units Int.instMonoid Int.instUnitsPow Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Equiv.injective SemigroupAction.mul_smul mul_comm
uzpow_natCast 📖	mathematical	—	Units Int.instMonoid Int.instUnitsPow AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring Nat.instCommSemiring AddCommMonoid.toNatModule Additive Additive.addCommMonoid CommGroup.toCommMonoid Units.instCommGroupUnits Int.instCommMonoid	—	Nat.cast_smul_eq_nsmul toMul_nsmul toMul_ofMul
uzpow_neg 📖	mathematical	—	Units Int.instMonoid Int.instUnitsPow CommRing.toCommSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Units.instInv	—	Equiv.injective neg_smul
uzpow_one 📖	mathematical	—	Units Int.instMonoid Int.instUnitsPow AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Equiv.injective one_smul
uzpow_sub 📖	mathematical	—	Units Int.instMonoid Int.instUnitsPow CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Units.instDiv	—	Equiv.injective sub_smul
uzpow_zero 📖	mathematical	—	Units Int.instMonoid Int.instUnitsPow MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Units.instOne	—	Equiv.injective zero_smul

---

← Back to Index