Basic

📁 Source: Mathlib/NumberTheory/MulChar/Basic.lean

Statistics

Metric	Count
Definitions MulChar, IsQuadratic, commGroup, equivToUnitHom, hasInv, hasMul, hasOne, inhabited, instFunLike, inv, mul, mulEquivToUnitHom, ofUnitHom, ringHomComp, toMonoidHom, toMonoidWithZeroHom, toUnitHom, trivial, MulCharClass	19
Theorems comp, eq_of_eq_coe, inv, pow_char, pow_even, pow_odd, sq_eq_one, coeToFun_mul, coe_equivToUnitHom, coe_mk, coe_toMonoidHom, coe_toUnitHom, eq_one_iff, equivToUnitHom_mul_apply, equivToUnitHom_symm_coe, ext, ext', ext_iff, injective_ringHomComp, instMulCharClass, inv_apply, inv_apply', inv_apply_eq_inv, inv_apply_eq_inv', inv_mul, isQuadratic_iff_sq_eq_one, map_nonunit, map_nonunit', map_one, map_ringChar, map_zero, mul_apply, mul_one, ne_one_iff, ofUnitHom_coe, ofUnitHom_eq, one_apply, one_apply_coe, one_mul, orderOf_pos, pow_apply', pow_apply_coe, pow_card_eq_one, ringHomComp_apply, ringHomComp_eq_one_iff, ringHomComp_inv, ringHomComp_mul, ringHomComp_ne_one_iff, ringHomComp_one, ringHomComp_pow, sum_eq_zero_of_ne_one, sum_one_eq_card_units, toMonoidWithZeroHom_apply, toUnitHom_eq, trivial_apply, val_neg_one_eq_one_of_odd_order, map_nonunit, toMonoidHomClass	58
Total	77

MulChar

Definitions

Name	Category	Theorems
IsQuadratic 📖	MathDef	5 math math: quadraticChar_isQuadratic, isQuadratic_iff_sq_eq_one, ZMod.isQuadratic_χ₈', ZMod.isQuadratic_χ₈, ZMod.isQuadratic_χ₄
commGroup 📖	CompOp	34 math math: DirichletCharacter.changeLevel_injective, exists_mulChar_orderOf, IsQuadratic.sq_eq_one, DirichletCharacter.changeLevel_def, DirichletCharacter.conductor_le_conductor_mem_conductorSet, DirichletCharacter.changeLevel_trans, DirichletCharacter.norm_LSeries_product_ge_one, IsQuadratic.pow_even, DirichletCharacter.LFunction_changeLevel, orderOf_dvd_card_sub_one, gaussSum_frob, DirichletCharacter.LSeries_changeLevel, pow_card_eq_one, DirichletCharacter.changeLevel_one, IsQuadratic.pow_char, pow_apply_coe, DirichletCharacter.changeLevel_toUnitHom, isQuadratic_iff_sq_eq_one, exists_mulChar_orderOf_eq_card_units, pow_apply', DirichletCharacter.changeLevel_factorsThrough, DirichletCharacter.norm_LFunction_product_ge_one, gaussSum_mul_gaussSum_pow_orderOf_sub_one, orderOf_pos, DirichletCharacter.changeLevel_eq_one_iff, DirichletCharacter.FactorsThrough.existsUnique, DirichletCharacter.changeLevel_self_toUnitHom, ringHomComp_pow, IsQuadratic.pow_odd, DirichletCharacter.changeLevel_primitiveCharacter, apply_mem_rootsOfUnity_orderOf, DirichletCharacter.changeLevel_self, DirichletCharacter.changeLevel_eq_cast_of_dvd, DirichletCharacter.FactorsThrough.eq_changeLevel
equivToUnitHom 📖	CompOp	6 math math: equivToUnitHom_mul_apply, toUnitHom_eq, equivToUnitHom_symm_coe, ofUnitHom_eq, coe_equivToUnitHom, apply_mem_rootsOfUnity
hasInv 📖	CompOp	15 math math: inv_apply_eq_inv, DirichletCharacter.IsPrimitive.completedLFunction_one_sub, inv_mul, IsQuadratic.inv, ringHomComp_inv, gaussSum_mulShift_of_isPrimitive, DirichletCharacter.IsPrimitive.fourierTransform_eq_inv_mul_gaussSum, star_apply', jacobiSum_nontrivial_inv, inv_apply_eq_inv', star_eq_inv, inv_apply', jacobiSum_mul_jacobiSum_inv, gaussSum_mul_gaussSum_eq_card, inv_apply
hasMul 📖	CompOp	13 math math: equivToUnitHom_mul_apply, jacobiSum_mul_nontrivial, one_mul, star_apply, mulEquiv_units, DirichletCharacter.mulEquiv_units, inv_mul, jacobiSum_eq_gaussSum_mul_gaussSum_div_gaussSum, mul_apply, ringHomComp_mul, star_eq_inv, mul_one, coeToFun_mul
hasOne 📖	CompOp	28 math math: IsQuadratic.sq_eq_one, DirichletCharacter.LSeries_modOne_eq, one_mul, DirichletCharacter.norm_LSeries_product_ge_one, one_apply_coe, IsQuadratic.pow_even, DirichletCharacter.primitiveCharacter_one, jacobiSum_one_nontrivial, DirichletCharacter.level_one', DirichletCharacter.conductor_one, pow_card_eq_one, DirichletCharacter.changeLevel_one, inv_mul, isQuadratic_iff_sq_eq_one, DirichletCharacter.level_one, sum_one_eq_card_units, eq_one_iff, DirichletCharacter.isPrimitive_one_level_one, DirichletCharacter.isPrimitive_one_level_zero, ringHomComp_eq_one_iff, one_apply, DirichletCharacter.eq_one_iff_conductor_eq_one, mul_one, DirichletCharacter.changeLevel_eq_one_iff, ringHomComp_one, DirichletCharacter.factorsThrough_one_iff, DirichletCharacter.conductor_one_dvd, jacobiSum_one_one
inhabited 📖	CompOp	—
instFunLike 📖	CompOp	147 math math: ArithmeticFunction.vonMangoldt.residueClass_eq, quadraticChar_card_sqrts, ZMod.χ₈'_int_eq_if_mod_eight, eq_iff, quadraticChar_card_card, DirichletCharacter.Odd.eval_neg, DirichletCharacter.LSeries_eulerProduct_tprod, exists_apply_eq_pow, map_one, apply_mem_algebraAdjoin_of_pow_eq_one, DirichletCharacter.LSeries_modOne_eq, DirichletCharacter.LSeriesSummable_of_one_lt_re, map_ringChar, DirichletCharacter.LSeries_twist_vonMangoldt_eq, quadraticChar_two, DirichletCharacter.LFunction_eq_LSeries, apply_mem_algebraAdjoin, DirichletCharacter.norm_LSeries_product_ge_one, inv_apply_eq_inv, one_apply_coe, DirichletCharacter.deriv_LFunction_eq_deriv_LSeries, DirichletCharacter.LFunction_changeLevel, gaussSum_mul, ZMod.χ₄_int_mod_four, star_apply, DirichletCharacter.norm_le_one, DirichletCharacter.mul_delta, DirichletCharacter.eval_modulus_sub, quadraticChar_dichotomy, ringHomComp_apply, ZMod.χ₈'_nat_eq_if_mod_eight, DirichletCharacter.unit_norm_eq_one, DirichletCharacter.Odd.to_fun, ZMod.χ₈'_int_eq_χ₄_mul_χ₈, DirichletCharacter.sum_characters_eq, ArithmeticFunction.vonMangoldt.residueClass_apply, DirichletCharacter.LSeriesSummable_mul, DirichletCharacter.LSeries_changeLevel, quadraticChar_sum_zero, equivToUnitHom_symm_coe, quadraticChar_eq_zero_iff, quadraticChar_zero, pow_apply_coe, mul_gaussSum_inv_eq_gaussSum, coe_mk, DirichletCharacter.toUnitHom_eq_char', apply_mem_rootsOfUnity_of_pow_eq_one, DirichletCharacter.LSeries.mul_mu_eq_one, sum_one_eq_card_units, DirichletCharacter.sum_char_inv_mul_char_eq, eq_one_iff, Char.card_pow_card, ZMod.χ₈'_eq_χ₄_mul_χ₈, val_neg_one_eq_one_of_odd_order, coe_toMonoidHom, legendreSym.at_two, gaussSum_aux_of_mulShift, quadraticChar_exists_neg_one', DirichletCharacter.summable_neg_log_one_sub_mul_prime_cpow, jacobiSym.at_neg_two, gaussSum_mulShift_of_isPrimitive, ZMod.χ₈_int_mod_eight, pow_apply', FiniteField.two_pow_card, quadraticChar_neg_two, IsQuadratic.gaussSum_frob_iter, DirichletCharacter.LSeriesSummable_twist_vonMangoldt, DirichletCharacter.modOne_eq_one, DirichletCharacter.convolution_twist_vonMangoldt, ZMod.χ₄_nat_one_mod_four, jacobiSym.neg, mul_apply, starComp_apply, DirichletCharacter.LSeriesSummable_iff, ZMod.χ₈_nat_mod_eight, DirichletCharacter.IsPrimitive.fourierTransform_eq_inv_mul_gaussSum, ZMod.χ₄_int_three_mod_four, DirichletCharacter.absicssaOfAbsConv_eq_one, star_apply', one_apply, ZMod.χ₄_nat_three_mod_four, DirichletCharacter.sum_characters_eq_zero, DirichletCharacter.mul_convolution_distrib, jacobiSum_nontrivial_inv, ZMod.χ₄_apply, inv_apply_eq_inv', ZMod.χ₄_int_one_mod_four, quadraticChar_eq_one_of_char_two, DirichletCharacter.LSeries_eulerProduct_hasProd, gaussSum_mul_gaussSum_pow_orderOf_sub_one, ZMod.χ₄_eq_neg_one_pow, tsum_dirichletSummand, jacobiSym.at_two, DirichletCharacter.LSeries_eulerProduct_exp_log, quadraticChar_sq_one, ArithmeticFunction.vonMangoldt.LSeries_residueClass_eq, legendreSym.at_neg_one, IsQuadratic.gaussSum_frob, quadraticChar_odd_prime, inv_apply', ofRootOfUnity_spec, map_nonunit, DirichletCharacter.apply_eq_toArithmeticFunction_apply, gaussSum_pow_eq_prod_jacobiSum, quadraticChar_sq_one', DirichletCharacter.not_LSeriesSummable_at_one, jacobiSum_eq_sum_sdiff, ZMod.χ₈'_apply, quadraticChar_apply, trivial_apply, legendreSym.at_neg_two, ZMod.χ₄_int_eq_if_mod_four, coe_toUnitHom, quadraticChar_neg_one_iff_not_isSquare, quadraticChar_eq_pow_of_char_ne_two, quadraticChar_eq_pow_of_char_ne_two', DirichletCharacter.delta_mul, ZMod.χ₄_nat_mod_four, ext_iff, DirichletCharacter.isMultiplicative_toArithmeticFunction, DirichletCharacter.convolution_mul_moebius, ofUnitHom_coe, quadraticChar_neg_one, DirichletCharacter.Even.to_fun, ZMod.χ₈_nat_eq_if_mod_eight, DirichletCharacter.map_zero', apply_mem_rootsOfUnity_orderOf, jacobiSym.at_neg_one, DirichletCharacter.modZero_eq_delta, DirichletCharacter.fourierTransform_eq_gaussSum_mulShift, coe_equivToUnitHom, map_zero, quadraticChar_eq_neg_one_iff_not_one, DirichletCharacter.LSeries_eulerProduct, instMulCharClass, coeToFun_mul, inv_apply, DirichletCharacter.changeLevel_eq_cast_of_dvd, sum_eq_zero_of_ne_one, gaussSum_sq, ZMod.χ₈_apply, quadraticChar_one_iff_isSquare, quadraticChar_exists_neg_one, ZMod.χ₄_nat_eq_if_mod_four, ZMod.χ₈_int_eq_if_mod_eight, DirichletCharacter.Even.eval_neg, gaussSum_mulShift
inv 📖	CompOp	—
mul 📖	CompOp	—
mulEquivToUnitHom 📖	CompOp	—
ofUnitHom 📖	CompOp	3 math math: DirichletCharacter.changeLevel_def, ofUnitHom_eq, ofUnitHom_coe
ringHomComp 📖	CompOp	9 math math: IsQuadratic.comp, injective_ringHomComp, ringHomComp_apply, ringHomComp_inv, ringHomComp_eq_one_iff, ringHomComp_mul, ringHomComp_pow, jacobiSum_ringHomComp, ringHomComp_one
toMonoidHom 📖	CompOp	3 math math: toMonoidWithZeroHom_apply, coe_toMonoidHom, map_nonunit'
toMonoidWithZeroHom 📖	CompOp	1 math math: toMonoidWithZeroHom_apply
toUnitHom 📖	CompOp	10 math math: toUnitHom_eq, DirichletCharacter.changeLevel_def, DirichletCharacter.toUnitHom_inj, DirichletCharacter.Even.toUnitHom_eval_neg_one, DirichletCharacter.toUnitHom_eq_char', DirichletCharacter.changeLevel_toUnitHom, DirichletCharacter.changeLevel_self_toUnitHom, coe_toUnitHom, DirichletCharacter.factorsThrough_iff_ker_unitsMap, DirichletCharacter.Odd.toUnitHom_eval_neg_one
trivial 📖	CompOp	2 math math: jacobiSum_trivial_trivial, trivial_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeToFun_mul 📖	mathematical	—	DFunLike.coe MulChar instFunLike hasMul Pi.instMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	—
coe_equivToUnitHom 📖	mathematical	—	Units.val MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero DFunLike.coe MonoidHom Units CommMonoid.toMonoid MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Equiv MulChar EquivLike.toFunLike Equiv.instEquivLike equivToUnitHom instFunLike	—	coe_toUnitHom
coe_mk 📖	mathematical	OneHom.toFun MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero MonoidHom.toOneHom MulZeroClass.toZero MulZeroOneClass.toMulZeroClass	DFunLike.coe MulChar instFunLike MonoidHom MonoidHom.instFunLike	—	—
coe_toMonoidHom 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero MonoidHom.instFunLike toMonoidHom MulChar instFunLike	—	—
coe_toUnitHom 📖	mathematical	—	Units.val MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero DFunLike.coe MonoidHom Units CommMonoid.toMonoid MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike toUnitHom MulChar instFunLike	—	—
eq_one_iff 📖	mathematical	—	MulChar hasOne DFunLike.coe instFunLike Units.val CommMonoid.toMonoid MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	one_apply_coe
equivToUnitHom_mul_apply 📖	mathematical	—	DFunLike.coe MonoidHom Units CommMonoid.toMonoid MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Equiv MulChar EquivLike.toFunLike Equiv.instEquivLike equivToUnitHom hasMul Units.instMul	—	Units.val_injective coe_equivToUnitHom
equivToUnitHom_symm_coe 📖	mathematical	—	DFunLike.coe MulChar instFunLike Equiv MonoidHom Units CommMonoid.toMonoid MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero MulOneClass.toMulOne Units.instMulOneClass EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivToUnitHom Units.val MonoidHom.instFunLike	—	ofUnitHom_coe
ext 📖	—	DFunLike.coe MulChar instFunLike Units.val CommMonoid.toMonoid	—	—	ext' map_nonunit
ext' 📖	—	DFunLike.coe MulChar instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe MulChar instFunLike Units.val CommMonoid.toMonoid	—	ext
injective_ringHomComp 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	MulChar CommSemiring.toCommMonoidWithZero ringHomComp	—	—
instMulCharClass 📖	mathematical	—	MulCharClass MulChar instFunLike	—	MonoidHom.map_mul' OneHom.map_one' map_nonunit'
inv_apply 📖	mathematical	—	DFunLike.coe MulChar CommMonoidWithZero.toCommMonoid instFunLike hasInv Ring.inverse CommMonoidWithZero.toMonoidWithZero	—	inv_apply_eq_inv IsUnit.map MulCharClass.toMonoidHomClass instMulCharClass IsUnit.mul_right_injective Ring.mul_inverse_cancel map_mul MonoidHomClass.toMulHomClass map_one MonoidHomClass.toOneHomClass Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton instIsEmptyFalse map_nonunit Ring.inverse_non_unit map_zero
inv_apply' 📖	mathematical	—	DFunLike.coe MulChar CommMonoidWithZero.toCommMonoid CommGroupWithZero.toCommMonoidWithZero instFunLike hasInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid	—	inv_apply Ring.inverse_eq_inv
inv_apply_eq_inv 📖	mathematical	—	DFunLike.coe MulChar instFunLike hasInv Ring.inverse CommMonoidWithZero.toMonoidWithZero	—	—
inv_apply_eq_inv' 📖	mathematical	—	DFunLike.coe MulChar CommGroupWithZero.toCommMonoidWithZero instFunLike hasInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid	—	inv_apply_eq_inv Ring.inverse_eq_inv
inv_mul 📖	mathematical	—	MulChar hasMul hasInv hasOne	—	ext coeToFun_mul Pi.mul_apply inv_apply_eq_inv Ring.inverse_mul_cancel IsUnit.map MulCharClass.toMonoidHomClass instMulCharClass Units.isUnit one_apply_coe
isQuadratic_iff_sq_eq_one 📖	mathematical	—	IsQuadratic MulChar CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup commGroup hasOne	—	ext one_apply_coe pow_apply_coe not_isUnit_zero IsUnit.map MulCharClass.toMonoidHomClass instMulCharClass Units.isUnit one_pow Even.neg_pow Nat.instAtLeastTwoHAddOfNat sq_eq_one_iff pow_apply' two_ne_zero one_apply map_nonunit
map_nonunit 📖	mathematical	IsUnit CommMonoid.toMonoid	DFunLike.coe MulChar instFunLike MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	map_nonunit'
map_nonunit' 📖	mathematical	IsUnit CommMonoid.toMonoid	OneHom.toFun MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero MonoidHom.toOneHom toMonoidHom MulZeroClass.toZero MulZeroOneClass.toMulZeroClass	—	—
map_one 📖	mathematical	—	DFunLike.coe MulChar instFunLike MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	OneHom.map_one'
map_ringChar 📖	mathematical	—	DFunLike.coe MulChar CommSemiring.toCommMonoid instFunLike AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring ringChar MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	ringChar.Nat.cast_ringChar map_zero
map_zero 📖	mathematical	—	DFunLike.coe MulChar CommMonoidWithZero.toCommMonoid instFunLike MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	map_nonunit not_isUnit_zero
mul_apply 📖	mathematical	—	DFunLike.coe MulChar instFunLike hasMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	—
mul_one 📖	mathematical	—	MulChar hasMul hasOne	—	ext one_apply_coe mul_one
ne_one_iff 📖	—	—	—	—	—
ofUnitHom_coe 📖	mathematical	—	DFunLike.coe MulChar instFunLike ofUnitHom Units.val CommMonoid.toMonoid MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero MonoidHom Units MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike	—	IsUnit.unit_of_val_units
ofUnitHom_eq 📖	mathematical	—	ofUnitHom DFunLike.coe Equiv MonoidHom Units CommMonoid.toMonoid MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero MulOneClass.toMulOne Units.instMulOneClass MulChar EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivToUnitHom	—	—
one_apply 📖	mathematical	IsUnit CommMonoid.toMonoid	DFunLike.coe MulChar instFunLike hasOne MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	one_apply_coe
one_apply_coe 📖	mathematical	—	DFunLike.coe MulChar instFunLike hasOne Units.val CommMonoid.toMonoid MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	Units.isUnit
one_mul 📖	mathematical	—	MulChar hasMul hasOne	—	ext one_apply_coe one_mul
orderOf_pos 📖	mathematical	—	orderOf MulChar DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup commGroup	—	nonempty_fintype IsOfFinOrder.orderOf_pos isOfFinOrder_iff_pow_eq_one Fintype.card_pos pow_card_eq_one
pow_apply' 📖	mathematical	—	DFunLike.coe MulChar instFunLike Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup commGroup MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	—	pow_apply_coe map_nonunit zero_pow
pow_apply_coe 📖	mathematical	—	DFunLike.coe MulChar instFunLike Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup commGroup Units.val CommMonoid.toMonoid MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	—	pow_zero one_apply_coe pow_succ mul_apply
pow_card_eq_one 📖	mathematical	—	MulChar Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup commGroup Fintype.card Units CommMonoid.toMonoid hasOne	—	ext pow_apply_coe map_pow MulCharClass.toMonoidHomClass instMulCharClass one_apply_coe Units.val_pow_eq_pow_val pow_card_eq_one Units.val_eq_one map_one MonoidHomClass.toOneHomClass
ringHomComp_apply 📖	mathematical	—	DFunLike.coe MulChar CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring instFunLike ringHomComp RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	—	—
ringHomComp_eq_one_iff 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	ringHomComp MulChar CommSemiring.toCommMonoidWithZero hasOne	—	ringHomComp_one injective_ringHomComp
ringHomComp_inv 📖	mathematical	—	MulChar CommMonoidWithZero.toCommMonoid CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring hasInv ringHomComp	—	ext inv_apply Ring.inverse_unit
ringHomComp_mul 📖	mathematical	—	ringHomComp MulChar CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring hasMul	—	ext map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass
ringHomComp_ne_one_iff 📖	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	—	Iff.not ringHomComp_eq_one_iff
ringHomComp_one 📖	mathematical	—	ringHomComp MulChar CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring hasOne	—	ext one_apply_coe map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
ringHomComp_pow 📖	mathematical	—	MulChar CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup commGroup ringHomComp	—	pow_zero ringHomComp_one pow_succ ringHomComp_mul
sum_eq_zero_of_ne_one 📖	mathematical	—	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ DFunLike.coe MulChar CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	ne_one_iff eq_zero_of_mul_eq_self_left IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Finset.mul_sum Finset.sum_congr MonoidHomClass.toMulHomClass MulCharClass.toMonoidHomClass instMulCharClass Function.Bijective.sum_comp Units.mulLeft_bijective
sum_one_eq_card_units 📖	mathematical	—	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ DFunLike.coe MulChar CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring instFunLike hasOne AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Fintype.card Units CommMonoid.toMonoid instFintypeUnitsOfDecidableEq	—	Units.val_injective Finset.sum_congr one_apply_coe map_nonunit Finset.sum_boole Finset.ext Finset.card_map
toMonoidWithZeroHom_apply 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero MonoidWithZeroHom.funLike toMonoidWithZeroHom OneHom.toFun MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid CommMonoidWithZero.toCommMonoid MulZeroOneClass.toMulOneClass MonoidHom.toOneHom toMonoidHom	—	—
toUnitHom_eq 📖	mathematical	—	toUnitHom DFunLike.coe Equiv MulChar MonoidHom Units CommMonoid.toMonoid MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero MulOneClass.toMulOne Units.instMulOneClass EquivLike.toFunLike Equiv.instEquivLike equivToUnitHom	—	—
trivial_apply 📖	mathematical	—	DFunLike.coe MulChar instFunLike trivial IsUnit CommMonoid.toMonoid IsUnit.instDecidableOfExistsUnitsEqVal Units Units.val MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass	—	—
val_neg_one_eq_one_of_odd_order 📖	mathematical	Odd Nat.instSemiring MulChar CommRing.toCommMonoid Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup commGroup hasOne	DFunLike.coe instFunLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	Odd.neg_one_pow map_pow MulCharClass.toMonoidHomClass instMulCharClass pow_apply' Nat.ne_of_odd_add one_apply_coe

MulChar.IsQuadratic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	MulChar.IsQuadratic	MulChar.ringHomComp	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass map_neg RingHomClass.toAddMonoidHomClass
eq_of_eq_coe 📖	—	MulChar.IsQuadratic Int.instCommRing CommRing.toCommMonoid AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe MulChar CommSemiring.toCommMonoidWithZero Int.instCommSemiring MulChar.instFunLike	—	—	Int.cast_injOn_of_ringChar_ne_two
inv 📖	mathematical	MulChar.IsQuadratic	MulChar CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring MulChar.hasInv	—	MulChar.ext MulChar.inv_apply_eq_inv Ring.inverse_zero Ring.inverse_one Nat.cast_one Int.cast_neg Int.cast_one Ring.inverse_unit inv_neg inv_one
pow_char 📖	mathematical	MulChar.IsQuadratic	MulChar CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulChar.commGroup	—	MulChar.ext MulChar.pow_apply_coe zero_pow Nat.Prime.ne_zero Fact.out one_pow neg_one_pow_char
pow_even 📖	mathematical	MulChar.IsQuadratic Even	MulChar CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulChar.commGroup MulChar.hasOne	—	Nat.instAtLeastTwoHAddOfNat even_iff_two_dvd pow_mul sq_eq_one one_pow
pow_odd 📖	mathematical	MulChar.IsQuadratic Odd Nat.instSemiring	MulChar CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulChar.commGroup	—	pow_add pow_one Nat.instAtLeastTwoHAddOfNat pow_even even_two_mul one_mul
sq_eq_one 📖	mathematical	MulChar.IsQuadratic	MulChar CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulChar.commGroup MulChar.hasOne	—	inv_mul_cancel pow_two inv

MulCharClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_nonunit 📖	mathematical	IsUnit CommMonoid.toMonoid	DFunLike.coe MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	—
toMonoidHomClass 📖	mathematical	—	MonoidHomClass MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	—

(root)

Definitions

Name	Category	Theorems
MulChar 📖	CompData	127 math math: MulChar.equivToUnitHom_mul_apply, quadraticChar_card_sqrts, ZMod.χ₈'_int_eq_if_mod_eight, MulChar.eq_iff, quadraticChar_card_card, MulChar.toUnitHom_eq, MulChar.exists_mulChar_orderOf, MulChar.IsQuadratic.sq_eq_one, MulChar.map_one, MulChar.map_ringChar, jacobiSum_mul_nontrivial, MulChar.injective_ringHomComp, quadraticChar_two, MulChar.one_mul, MulChar.inv_apply_eq_inv, MulChar.one_apply_coe, MulChar.IsQuadratic.pow_even, gaussSum_mul, ZMod.χ₄_int_mod_four, MulChar.star_apply, quadraticChar_dichotomy, MulChar.mulEquiv_units, MulChar.ringHomComp_apply, ZMod.χ₈'_nat_eq_if_mod_eight, jacobiSum_one_nontrivial, ZMod.χ₈'_int_eq_χ₄_mul_χ₈, MulChar.orderOf_dvd_card_sub_one, gaussSum_frob, quadraticChar_sum_zero, MulChar.equivToUnitHom_symm_coe, MulChar.pow_card_eq_one, quadraticChar_eq_zero_iff, MulChar.IsQuadratic.pow_char, MulChar.inv_mul, quadraticChar_zero, MulChar.pow_apply_coe, mul_gaussSum_inv_eq_gaussSum, MulChar.coe_mk, MulChar.IsQuadratic.inv, MulChar.isQuadratic_iff_sq_eq_one, MulChar.sum_one_eq_card_units, MulChar.exists_mulChar_orderOf_eq_card_units, MulChar.eq_one_iff, Char.card_pow_card, ZMod.χ₈'_eq_χ₄_mul_χ₈, MulChar.coe_toMonoidHom, legendreSym.at_two, quadraticChar_exists_neg_one', MulChar.ringHomComp_inv, jacobiSym.at_neg_two, ZMod.χ₈_int_mod_eight, MulChar.pow_apply', FiniteField.two_pow_card, quadraticChar_neg_two, MulChar.IsQuadratic.gaussSum_frob_iter, MulChar.finite, jacobiSum_eq_gaussSum_mul_gaussSum_div_gaussSum, ZMod.χ₄_nat_one_mod_four, jacobiSym.neg, MulChar.mul_apply, MulChar.starComp_apply, MulChar.ofUnitHom_eq, ZMod.χ₈_nat_mod_eight, MulChar.ringHomComp_eq_one_iff, ZMod.χ₄_int_three_mod_four, MulChar.ringHomComp_mul, MulChar.star_apply', MulChar.one_apply, ZMod.χ₄_nat_three_mod_four, jacobiSum_nontrivial_inv, ZMod.χ₄_apply, MulChar.inv_apply_eq_inv', ZMod.χ₄_int_one_mod_four, quadraticChar_eq_one_of_char_two, gaussSum_mul_gaussSum_pow_orderOf_sub_one, ZMod.χ₄_eq_neg_one_pow, jacobiSym.at_two, quadraticChar_sq_one, MulChar.star_eq_inv, MulChar.orderOf_pos, legendreSym.at_neg_one, MulChar.IsQuadratic.gaussSum_frob, MulChar.mul_one, quadraticChar_odd_prime, MulChar.card_eq_card_units_of_hasEnoughRootsOfUnity, MulChar.inv_apply', MulChar.ofRootOfUnity_spec, MulChar.map_nonunit, quadraticChar_sq_one', MulChar.ringHomComp_pow, jacobiSum_eq_sum_sdiff, ZMod.χ₈'_apply, quadraticChar_apply, MulChar.trivial_apply, jacobiSum_mul_jacobiSum_inv, legendreSym.at_neg_two, ZMod.χ₄_int_eq_if_mod_four, MulChar.coe_toUnitHom, quadraticChar_neg_one_iff_not_isSquare, quadraticChar_eq_pow_of_char_ne_two, quadraticChar_eq_pow_of_char_ne_two', ZMod.χ₄_nat_mod_four, MulChar.ringHomComp_one, MulChar.ext_iff, MulChar.ofUnitHom_coe, quadraticChar_neg_one, MulChar.IsQuadratic.pow_odd, ZMod.χ₈_nat_eq_if_mod_eight, MulChar.apply_mem_rootsOfUnity_orderOf, jacobiSym.at_neg_one, MulChar.coe_equivToUnitHom, MulChar.map_zero, quadraticChar_eq_neg_one_iff_not_one, MulChar.instMulCharClass, MulChar.coeToFun_mul, gaussSum_mul_gaussSum_eq_card, MulChar.inv_apply, MulChar.apply_mem_rootsOfUnity, MulChar.sum_eq_zero_of_ne_one, gaussSum_sq, ZMod.χ₈_apply, jacobiSum_one_one, quadraticChar_one_iff_isSquare, quadraticChar_exists_neg_one, ZMod.χ₄_nat_eq_if_mod_four, ZMod.χ₈_int_eq_if_mod_eight, gaussSum_mulShift
MulCharClass 📖	CompData	1 math math: MulChar.instMulCharClass

---

← Back to Index