Documentation Verification Report

BoundedContinuousFunctionChar

📁 Source: Mathlib/Analysis/Fourier/BoundedContinuousFunctionChar.lean

Statistics

Metric	Count
Definitions `char`, `charAlgHom`, `charMonoidHom`, `charPoly`	4
Theorems `charAlgHom_apply`, `charMonoidHom_apply`, `char_add_eq_mul`, `char_apply`, `char_mem_charPoly`, `char_neg`, `char_zero_eq_one`, `ext_of_char_eq`, `mem_charPoly`, `separatesPoints_charPoly`, `star_mem_range_charAlgHom`	11
Total	15

BoundedContinuousFunction

Definitions

Name	Category	Theorems
`char` 📖	CompOp	5 math math: `char_neg`, `char_zero_eq_one`, `char_add_eq_mul`, `char_mem_charPoly`, `char_apply`
`charAlgHom` 📖	CompOp	1 math math: `charAlgHom_apply`
`charMonoidHom` 📖	CompOp	1 math math: `charMonoidHom_apply`
`charPoly` 📖	CompOp	3 math math: `mem_charPoly`, `separatesPoints_charPoly`, `char_mem_charPoly`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charAlgHom_apply` 📖	mathematical	`Continuous` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `DFunLike.coe` `AddChar` `Real.instAddMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `instTopologicalSpaceProd` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`BoundedContinuousFunction` `Complex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `instFunLike` `AlgHom` `AddMonoidAlgebra` `Complex.instSemiring` `Complex.instCommSemiring` `AddMonoidAlgebra.semiring` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instSemiring` `instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex.instNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `AddMonoidAlgebra.algebra` `instAlgebra` `NormedCommRing.toNormedRing` `NormedAlgebra.id` `AlgHom.funLike` `charAlgHom` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Complex.instMul` `Finsupp` `Finsupp.instFunLike` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Ring.toSemiring` `SeminormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.unitSphere`	—	`Algebra.to_smulCommClass` `instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `AddMonoidAlgebra.lift_apply` `Finsupp.sum_of_support_subset` `subset_rfl` `Finset.instReflSubset` `zero_smul` `NormedSpace.toIsBoundedSMul` `coe_sum` `Finset.sum_congr` `charMonoidHom_apply` `Finset.sum_apply`
`charMonoidHom_apply` 📖	mathematical	`Continuous` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `DFunLike.coe` `AddChar` `Real.instAddMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `instTopologicalSpaceProd` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`BoundedContinuousFunction` `Complex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `instFunLike` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Complex.instSemiring` `instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `MonoidHom.instFunLike` `charMonoidHom` `Submonoid` `Ring.toSemiring` `SeminormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.unitSphere`	—	`Algebra.to_smulCommClass`
`char_add_eq_mul` 📖	mathematical	`Continuous` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `DFunLike.coe` `AddChar` `Real.instAddMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `instTopologicalSpaceProd` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`char` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `BoundedContinuousFunction` `Complex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `instMul` `Complex.instMul` `instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing`	—	`Algebra.to_smulCommClass` `ext` `instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `AddChar.map_add_eq_mul`
`char_apply` 📖	mathematical	`Continuous` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `DFunLike.coe` `AddChar` `Real.instAddMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `instTopologicalSpaceProd` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`BoundedContinuousFunction` `Complex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `instFunLike` `char` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Ring.toSemiring` `SeminormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.unitSphere`	—	`Algebra.to_smulCommClass`
`char_mem_charPoly` 📖	mathematical	`Continuous` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `DFunLike.coe` `AddChar` `Real.instAddMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `instTopologicalSpaceProd` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`BoundedContinuousFunction` `Complex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `StarSubalgebra` `Complex.instCommSemiring` `Complex.instStarRing` `instSemiring` `Complex.instSemiring` `instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex.instNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `instStarRing` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `CStarRing.to_normedStarGroup` `RCLike.instCStarRing` `Complex.instRCLike` `instAlgebra` `NormedCommRing.toNormedRing` `NormedAlgebra.id` `instStarModule` `StarRing.toStarAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `RCLike.innerProductSpace` `StarMul.toStarModule` `CommRing.toCommMonoid` `Complex.commRing` `StarRing.toStarMul` `SetLike.instMembership` `StarSubalgebra.setLike` `charPoly` `char`	—	`Algebra.to_smulCommClass` `instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `CStarRing.to_normedStarGroup` `RCLike.instCStarRing` `instStarModule` `StarMul.toStarModule` `mem_charPoly` `Finset.sum_congr` `Finset.sum_eq_single` `NeZero.charZero_one` `Complex.instCharZero` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Finsupp.single_eq_same` `one_mul`
`char_neg` 📖	mathematical	`Continuous` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `DFunLike.coe` `AddChar` `Real.instAddMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `instTopologicalSpaceProd` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`char` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Star.star` `BoundedContinuousFunction` `Complex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `instAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instStarAddMonoid` `StarRing.toStarAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Complex.instStarRing` `CStarRing.to_normedStarGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `RCLike.instCStarRing` `Complex.instRCLike`	—	`Algebra.to_smulCommClass` `ext` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `CStarRing.to_normedStarGroup` `RCLike.instCStarRing` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Circle.star_addChar`
`char_zero_eq_one` 📖	mathematical	`Continuous` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `DFunLike.coe` `AddChar` `Real.instAddMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `instTopologicalSpaceProd` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`char` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `BoundedContinuousFunction` `Complex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `instOne` `Complex.instOne`	—	`Algebra.to_smulCommClass` `ext` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `AddChar.map_zero_eq_one`
`ext_of_char_eq` 📖	—	`Continuous` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `DFunLike.coe` `AddChar` `Real.instAddMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `instTopologicalSpaceProd` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `BoundedContinuousFunction` `Complex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `instFunLike` `char`	—	—	`Algebra.to_smulCommClass` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `DFunLike.ne_iff` `sub_ne_zero_of_ne` `char.congr_simp` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `div_eq_one_iff_eq` `Circle.coe_ne_zero` `div_eq_inv_mul` `Metric.unitSphere.coe_inv` `AddChar.map_neg_eq_inv` `Submonoid.coe_mul` `AddChar.map_add_eq_mul` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `OneMemClass.coe_eq_one` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass`
`mem_charPoly` 📖	mathematical	`Continuous` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `DFunLike.coe` `AddChar` `Real.instAddMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `instTopologicalSpaceProd` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`BoundedContinuousFunction` `Complex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `StarSubalgebra` `Complex.instCommSemiring` `Complex.instStarRing` `instSemiring` `Complex.instSemiring` `instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex.instNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `instStarRing` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `CStarRing.to_normedStarGroup` `RCLike.instCStarRing` `Complex.instRCLike` `instAlgebra` `NormedCommRing.toNormedRing` `NormedAlgebra.id` `instStarModule` `StarRing.toStarAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `RCLike.innerProductSpace` `StarMul.toStarModule` `CommRing.toCommMonoid` `Complex.commRing` `StarRing.toStarMul` `SetLike.instMembership` `StarSubalgebra.setLike` `charPoly` `instFunLike` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Complex.instMul` `Finsupp` `Finsupp.instFunLike` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Ring.toSemiring` `SeminormedRing.toRing` `Submonoid.instSetLike` `Submonoid.unitSphere`	—	`Algebra.to_smulCommClass` `instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `CStarRing.to_normedStarGroup` `RCLike.instCStarRing` `instStarModule` `StarMul.toStarModule` `charAlgHom_apply`
`separatesPoints_charPoly` 📖	mathematical	`Continuous` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `DFunLike.coe` `AddChar` `Real.instAddMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `instTopologicalSpaceProd` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`Subalgebra.SeparatesPoints` `Complex` `Complex.instCommSemiring` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Ring.toSemiring` `NormedRing.toRing` `NormedAlgebra.toAlgebra` `NormedAlgebra.id` `IsTopologicalRing.toIsTopologicalSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `StarSubalgebra.toSubalgebra` `ContinuousMap` `Complex.instStarRing` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `ContinuousMap.instStarRingOfContinuousStar` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.instContinuousStar` `ContinuousMap.algebra` `ContinuousMap.instStarModule` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `Algebra.toSMul` `StarMul.toStarModule` `CommRing.toCommMonoid` `Complex.commRing` `StarRing.toStarMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `StarSubalgebra.map` `BoundedContinuousFunction` `SeminormedCommRing.toSeminormedRing` `instSemiring` `Complex.instSemiring` `instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex.instNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `instStarRing` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `CStarRing.to_normedStarGroup` `RCLike.instCStarRing` `Complex.instRCLike` `instAlgebra` `instStarModule` `RCLike.innerProductSpace` `toContinuousMapStarₐ` `charPoly`	—	`Algebra.to_smulCommClass` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.instContinuousStar` `ContinuousMap.instStarModule` `StarMul.toStarModule` `instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `CStarRing.to_normedStarGroup` `RCLike.instCStarRing` `instStarModule` `Mathlib.Tactic.Contrapose.contrapose₂` `ext_of_char_eq` `char_mem_charPoly`
`star_mem_range_charAlgHom` 📖	mathematical	`Continuous` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `DFunLike.coe` `AddChar` `Real.instAddMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `instTopologicalSpaceProd` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `BoundedContinuousFunction` `Complex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Subalgebra` `Complex.instCommSemiring` `instSemiring` `Complex.instSemiring` `instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex.instNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `instAlgebra` `NormedCommRing.toNormedRing` `NormedAlgebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `AddMonoidAlgebra` `AddMonoidAlgebra.semiring` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidAlgebra.algebra` `charAlgHom`	`Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `instAddMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instStarAddMonoid` `StarRing.toStarAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Complex.instStarRing` `CStarRing.to_normedStarGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `RCLike.instCStarRing` `Complex.instRCLike`	—	`Algebra.to_smulCommClass` `instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `CStarRing.to_normedStarGroup` `RCLike.instCStarRing` `star_zero` `ext` `charAlgHom_apply` `Finset.sum_map` `Finset.sum_congr` `Finsupp.embDomain_apply_self` `star_sum` `star_mul'` `Circle.star_addChar` `Finsupp.support_mapRange_of_injective` `star_injective` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`

---

← Back to Index