Documentation Verification Report

Frobenius

📁 Source: Mathlib/RingTheory/Frobenius.lean

Statistics

Metric	Count
Definitions `IsArithFrobAt`, `localize`, `restrict`, `IsArithFrobAt`, `arithFrobAt`	5
Theorems `apply_of_pow_eq_one`, `card_pos`, `comap_eq`, `eq_of_isUnramifiedAt`, `finite_quotient`, `isArithFrobAt_localize`, `le_comap`, `localize_algebraMap`, `mk_apply`, `restrict_apply`, `restrict_injective`, `restrict_mk`, `arithFrobAt`, `conj`, `exists_of_isInvariant`, `exists_primesOver_isConj`, `mul_inv_mem_inertia`, `isConj_arithFrobAt`	18
Total	23

AlgHom

Definitions

Name	Category	Theorems
`IsArithFrobAt` 📖	MathDef	—

AlgHom.IsArithFrobAt

Definitions

Name	Category	Theorems
`localize` 📖	CompOp	2 math math: `localize_algebraMap`, `isArithFrobAt_localize`
`restrict` 📖	CompOp	3 math math: `restrict_injective`, `restrict_mk`, `restrict_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_of_pow_eq_one` 📖	mathematical	`AlgHom.IsArithFrobAt` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `AddMonoidWithOne.toNatCast`	`DFunLike.coe` `AlgHom` `AlgHom.funLike` `Nat.card` `HasQuotient.Quotient` `Ideal.instHasQuotient_1` `Ideal.under`	—	`Nat.cast_zero` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `IsPrimitiveRoot.exists_pos` `Ideal.mem_of_dvd` `Nat.cast_dvd_cast` `IsPrimitiveRoot.dvd_of_pow_eq_one` `LT.lt.ne'` `IsPrimitiveRoot.eq_pow_of_pow_eq_one` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `IsPrimitiveRoot.pow_eq_one` `map_one` `MonoidHomClass.toOneHomClass` `Ideal.mul_unit_mem_iff_mem` `IsUnit.pow` `IsPrimitiveRoot.isUnit` `sub_mul` `one_mul` `pow_add` `add_mul` `Distrib.rightDistribClass` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.neg_add` `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_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.mul_neg` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `Int.instCharZero` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Linarith.natCast_nonneg` `Nat.cast_add` `pow_mul` `one_pow` `mul_one` `mul_comm` `sum_mem` `geom_sum_mul` `sub_eq_zero` `mul_eq_zero` `IsDomain.to_noZeroDivisors` `sub_self` `pow_right_comm` `Finset.sum_congr` `Finset.sum_sub_distrib` `Finset.sum_const` `Finset.card_range` `nsmul_eq_mul` `sub_zero`
`card_pos` 📖	mathematical	`AlgHom.IsArithFrobAt`	`Nat.card` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.under`	—	`finite_quotient` `Nat.card_pos` `Ideal.Quotient.instNonemptyQuotient` `Ideal.instIsTwoSided_1`
`comap_eq` 📖	mathematical	`AlgHom.IsArithFrobAt`	`Ideal.comap` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`	—	`le_antisymm` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Ideal.instIsTwoSided_1` `Ideal.Quotient.eq_zero_iff_mem` `restrict_injective` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Ideal.mem_comap` `le_comap`
`eq_of_isUnramifiedAt` 📖	—	`AlgHom.IsArithFrobAt` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `Ideal.primeCompl` `nonZeroDivisors` `Semiring.toMonoidWithZero`	—	—	`Algebra.FormallyUnramified.ext_of_iInf` `Localization.AtPrime.isLocalRing` `Ideal.iInf_pow_eq_bot_of_isLocalRing` `IsLocalization.instIsNoetherianRingLocalization` `Ideal.IsPrime.ne_top'` `Ideal.IsMaximal.isPrime'` `IsLocalRing.maximalIdeal.isMaximal` `Ideal.instIsTwoSided_1` `mk_apply` `isArithFrobAt_localize` `AlgHom.ext` `IsLocalization.injective` `Localization.isLocalization` `localize_algebraMap`
`finite_quotient` 📖	mathematical	`AlgHom.IsArithFrobAt`	`Finite` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.under`	—	`not_finite` `Ideal.comap_top` `Finite.of_fintype` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Nat.card_eq_zero_of_infinite` `pow_zero` `zero_sub` `NonUnitalSubringClass.toNegMemClass` `instNonUnitalSubringClassIdeal`
`isArithFrobAt_localize` 📖	mathematical	`AlgHom.IsArithFrobAt`	`Localization.AtPrime` `CommRing.toCommSemiring` `OreLocalization.instCommRing` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `OreLocalization.instAlgebra` `localize` `IsLocalRing.maximalIdeal` `OreLocalization.instCommSemiring` `Localization.AtPrime.isLocalRing`	—	`RingHom.instRingHomClass` `Localization.AtPrime.isLocalRing` `IsScalarTower.algebraMap_eq` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Ideal.comap_comap` `Localization.AtPrime.comap_maximalIdeal` `Localization.isLocalization` `IsLocalization.exists_mk'_eq` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Localization.le_comap_primeCompl_iff` `ge_of_eq` `Submonoid.instSubmonoidClass` `Localization.localRingHom_mk'` `IsLocalization.mk'_sub` `IsLocalization.AtPrime.isLocalRing` `IsLocalization.AtPrime.mk'_mem_maximal_iff` `Ideal.instIsTwoSided_1` `map_sub` `RingHomClass.toAddMonoidHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `mk_apply` `map_pow` `sub_self`
`le_comap` 📖	mathematical	`AlgHom.IsArithFrobAt`	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.comap` `AlgHom` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`	—	`AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Ideal.instIsTwoSided_1` `Ideal.Quotient.eq_zero_iff_mem` `mk_apply` `zero_pow_eq` `LT.lt.ne'` `card_pos`
`localize_algebraMap` 📖	mathematical	`AlgHom.IsArithFrobAt`	`DFunLike.coe` `AlgHom` `Localization.AtPrime` `CommRing.toCommSemiring` `OreLocalization.instSemiring` `CommSemiring.toSemiring` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `OreLocalization.instAlgebra` `AlgHom.funLike` `localize` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Algebra.id`	—	`Localization.localRingHom_to_map` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `comap_eq`
`mk_apply` 📖	mathematical	`AlgHom.IsArithFrobAt`	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ideal.Quotient.semiring` `Nat.card` `Ideal.instHasQuotient_1` `Ideal.under`	—	`Ideal.instIsTwoSided_1` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Ideal.Quotient.eq`
`restrict_apply` 📖	mathematical	`AlgHom.IsArithFrobAt`	`DFunLike.coe` `AlgHom` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.under` `Ideal.Quotient.commSemiring` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotientComapRingHomAlgebraMap` `AlgHom.funLike` `restrict` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.card`	—	`Ideal.instIsTwoSided_1` `Ideal.Quotient.mk_surjective` `mk_apply`
`restrict_injective` 📖	mathematical	`AlgHom.IsArithFrobAt`	`HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `DFunLike.coe` `AlgHom` `Ideal.under` `Ideal.Quotient.commSemiring` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotientComapRingHomAlgebraMap` `AlgHom.funLike` `restrict`	—	`injective_iff_map_eq_zero` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `restrict_apply` `isReduced_of_noZeroDivisors` `Ideal.Quotient.noZeroDivisors` `Ideal.instIsTwoSided_1` `LT.lt.ne'` `card_pos`
`restrict_mk` 📖	mathematical	`AlgHom.IsArithFrobAt`	`DFunLike.coe` `AlgHom` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.under` `Ideal.Quotient.commSemiring` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotientComapRingHomAlgebraMap` `AlgHom.funLike` `restrict` `RingHom` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike`	—	`Ideal.instIsTwoSided_1`

IsArithFrobAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arithFrobAt` 📖	mathematical	—	`IsArithFrobAt` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `arithFrobAt`	—	`exists_primesOver_isConj`
`conj` 📖	mathematical	`IsArithFrobAt` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Ideal.pointwiseDistribMulAction`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `Ideal.comap_symm` `RingHom.instRingHomClass` `Ideal.comap_coe` `Ideal.under.eq_1` `Ideal.comap_comap` `AlgHom.comp_algebraMap` `Ideal.pointwise_smul_eq_comap` `Ideal.mem_comap` `SemigroupAction.mul_smul` `smul_sub` `inv_smul_smul` `smul_pow'`
`exists_of_isInvariant` 📖	mathematical	—	`IsArithFrobAt` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Algebra.IsInvariant.isIntegral` `Ideal.Quotient.maximal_of_isField` `Finite.isField_of_domain` `Ideal.Quotient.isDomain` `Ideal.instIsTwoSided_1` `CharP.exists` `Finite.of_injective` `RingHom.instRingHomClass` `Ideal.algebraMap_quotient_injective` `nonempty_fintype` `FiniteField.card` `Ideal.IsMaximal.under` `CharP.of_ringHom_of_ne_zero` `Ideal.Quotient.noZeroDivisors` `Ideal.IsPrime.under` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Nat.Prime.ne_zero` `PerfectField.toPerfectRing` `PerfectField.ofFinite` `RingEquiv.map_mul'` `RingEquiv.map_add'` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `FiniteField.pow_card` `Ideal.over_under` `Ideal.Quotient.stabilizerHom_surjective` `Ideal.Quotient.eq` `Nat.card_eq_fintype_card` `DFunLike.congr_fun`
`exists_primesOver_isConj` 📖	mathematical	`Finite` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Set` `Set.instMembership` `Ideal.primesOver`	`IsArithFrobAt` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `IsConj`	—	`Algebra.IsInvariant.exists_smul_of_under_eq` `Ideal.primesOver.isPrime` `Ideal.LiesOver.over` `exists_of_isInvariant` `conj` `IsConj.trans` `IsConj.symm` `isConj_iff`
`mul_inv_mem_inertia` 📖	mathematical	`IsArithFrobAt` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Ideal.inertia` `CommRing.toRing` `DistribMulAction.toMulAction` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MulSemiringAction.toDistribMulAction` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`SemigroupAction.mul_smul` `smul_inv_smul` `sub_sub_sub_cancel_right` `sub_mem` `Submodule.addSubgroupClass`

(root)

Definitions

Name	Category	Theorems
`IsArithFrobAt` 📖	MathDef	3 math math: `IsArithFrobAt.exists_primesOver_isConj`, `IsArithFrobAt.arithFrobAt`, `IsArithFrobAt.exists_of_isInvariant`
`arithFrobAt` 📖	CompOp	2 math math: `IsArithFrobAt.arithFrobAt`, `isConj_arithFrobAt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isConj_arithFrobAt` 📖	mathematical	`Ideal.under` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	`IsConj` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `arithFrobAt`	—	`Ideal.IsPrime.under` `IsArithFrobAt.exists_primesOver_isConj`

---

← Back to Index