Documentation Verification Report

Basic

📁 Source: Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `finite_adjoin_of_finite_of_isIntegral`, `finite_adjoin_simple_of_isIntegral`, `algebraMap`, `fg_adjoin_singleton`, `map`, `map_of_comp_eq`, `of_aeval_monic`, `of_pow`, `of_subring`, `pair`, `pair_iff`, `tower_top`, `isIntegral_iff`, `map`, `map_iff`, `of_comp`, `of_map`, `isIntegralElem_map`, `isIntegralElem_one`, `isIntegralElem_zero`, `span_range_natDegree_eq_adjoin`, `fg_adjoin_of_finite`, `isIntegral_algEquiv`, `isIntegral_algHom_iff`, `isIntegral_algebraMap`, `isIntegral_algebraMap_iff`, `isIntegral_iff_isIntegral_closure_finite`, `isIntegral_one`, `isIntegral_zero`, `isNoetherian_adjoin_finset`, `map_isIntegral_int`	31
Total	31

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_adjoin_of_finite_of_isIntegral` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`Module.Finite` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `adjoin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Subalgebra.toCommRing` `Subalgebra.instModuleSubtypeMem`	—	`Module.Finite.of_fg` `fg_adjoin_of_finite`
`finite_adjoin_simple_of_isIntegral` 📖	mathematical	`IsIntegral`	`Module.Finite` `Subalgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `adjoin` `Set` `Set.instSingletonSet` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial.instCommRingAdjoinSingleton` `Subalgebra.instModuleSubtypeMem`	—	`Module.Finite.of_fg` `IsIntegral.fg_adjoin_singleton`

IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`IsScalarTower.algebraMap_eq` `Polynomial.hom_eval₂` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`fg_adjoin_singleton` 📖	mathematical	`IsIntegral`	`Submodule.FG` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Algebra.toModule` `DFunLike.coe` `OrderEmbedding` `Subalgebra` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Subalgebra.instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderEmbedding` `Subalgebra.toSubmodule` `Algebra.adjoin` `Set` `Set.instSingletonSet`	—	`Submodule.span_range_natDegree_eq_adjoin` `Polynomial.aeval_def`
`map` 📖	mathematical	`IsIntegral`	`DFunLike.coe`	—	`eq_1` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.comp_algebraMap` `RingHom.IsIntegralElem.map`
`map_of_comp_eq` 📖	mathematical	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `algebraMap` `IsIntegral`	`DFunLike.coe` `RingHom` `RingHom.instFunLike`	—	`Polynomial.Monic.map` `Polynomial.eval_map` `Polynomial.map_map` `Polynomial.eval₂_at_apply` `RingHom.map_zero`
`of_aeval_monic` 📖	—	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsIntegral` `CommRing.toRing` `DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval`	—	—	`Polynomial.Monic.comp` `Polynomial.eval₂_comp` `Polynomial.aeval_def`
`of_pow` 📖	—	`IsIntegral` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	—	—	`Polynomial.Monic.expand` `Polynomial.aeval_def` `Polynomial.expand_aeval`
`of_subring` 📖	—	`IsIntegral` `Subring` `CommRing.toRing` `SetLike.instMembership` `Subring.instSetLike` `Subring.toCommRing` `Algebra.ofSubring`	—	—	`tower_top` `Subring.instIsScalarTowerSubtypeMem` `IsScalarTower.left`
`pair` 📖	mathematical	`IsIntegral`	`Prod.instRing` `Prod.algebra` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`Polynomial.Monic.mul` `Polynomial.aeval_def` `Polynomial.aeval_prod_apply` `Polynomial.aeval_mul` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero`
`pair_iff` 📖	mathematical	—	`IsIntegral` `Prod.instRing` `Prod.algebra` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`map` `Prod.isScalarTower` `IsScalarTower.left` `AlgHom.algHomClass` `pair`
`tower_top` 📖	—	`IsIntegral`	—	—	`Polynomial.Monic.map` `Polynomial.aeval_def` `Polynomial.aeval_map_algebraMap`

RingEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIntegral_iff` 📖	mathematical	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `algebraMap` `toRingHom`	`IsIntegral`	—	`IsIntegral.tower_top` `Algebra.smul_def` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `mul_assoc` `RingEquivClass.toRingHomClass` `instRingEquivClass` `comp_symm` `RingHomCompTriple.comp_eq` `RingHomCompTriple.ids`

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIntegralElem_map` 📖	mathematical	—	`IsIntegralElem` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `instFunLike`	—	`Polynomial.monic_X_sub_C` `Polynomial.eval₂_sub` `Polynomial.eval₂_X` `Polynomial.eval₂_C` `sub_self`
`isIntegralElem_one` 📖	mathematical	—	`IsIntegralElem` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`isIntegralElem_map` `map_one`
`isIntegralElem_zero` 📖	mathematical	—	`IsIntegralElem` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`isIntegralElem_map` `map_zero`

RingHom.IsIntegralElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map` 📖	mathematical	`RingHom.IsIntegralElem`	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	—	`Polynomial.eval₂_eq_eval_map` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`map_iff` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	`RingHom.IsIntegralElem` `RingHom.comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`of_map` `map`
`of_comp` 📖	—	`RingHom.IsIntegralElem` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring`	—	—	`Polynomial.Monic.map` `Polynomial.eval₂_eq_eval_map` `Polynomial.map_map`
`of_map` 📖	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike` `RingHom.IsIntegralElem` `RingHom.comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	—	`Polynomial.hom_eval₂` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`span_range_natDegree_eq_adjoin` 📖	mathematical	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`span` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.image` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Finset.range` `Polynomial.natDegree` `OrderEmbedding` `Subalgebra` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Subalgebra.instPartialOrder` `instPartialOrder` `instFunLikeOrderEmbedding` `Subalgebra.toSubmodule` `Algebra.adjoin` `Set` `Set.instSingletonSet`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Finset.coe_image` `Finset.coe_range` `Unique.instSubsingleton` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `one_ne_zero'` `NeZero.one` `LE.le.antisymm` `span_le` `Finset.mem_image` `SetLike.mem_coe` `Subalgebra.pow_mem` `Algebra.subset_adjoin` `AlgHom.mem_range` `Algebra.adjoin_singleton_eq_range_aeval` `Subalgebra.mem_toSubmodule` `Polynomial.modByMonic_add_div` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `MulZeroClass.zero_mul` `add_zero` `Polynomial.sum_C_mul_X_pow_eq` `Polynomial.aeval_def` `Polynomial.eval₂_sum` `Polynomial.sum_def` `sum_mem` `addSubmonoidClass` `Polynomial.C_mul_X_pow_eq_monomial` `Polynomial.eval₂_monomial` `Algebra.smul_def` `smul_mem` `subset_span` `Finset.mem_image_of_mem` `Finset.mem_range` `LE.le.trans_lt` `Polynomial.le_natDegree_of_mem_supp` `Polynomial.natDegree_modByMonic_lt`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg_adjoin_of_finite` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`Submodule.FG` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `DFunLike.coe` `OrderEmbedding` `Subalgebra` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Subalgebra.instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderEmbedding` `Subalgebra.toSubmodule` `Algebra.adjoin`	—	`Set.Finite.induction_on` `Submodule.ext` `Algebra.adjoin_empty` `Finset.coe_singleton` `Submodule.one_eq_span` `Algebra.toSubmodule_bot` `Set.union_singleton` `IsScalarTower.right` `Algebra.adjoin_union_coe_submodule` `Submodule.FG.mul` `Set.mem_insert_of_mem` `IsIntegral.fg_adjoin_singleton` `Set.mem_insert`
`isIntegral_algEquiv` 📖	mathematical	—	`IsIntegral` `DFunLike.coe` `AlgEquiv` `CommRing.toCommSemiring` `Ring.toSemiring` `AlgEquiv.instFunLike`	—	`AlgEquiv.symm_apply_apply` `IsIntegral.map` `IsScalarTower.left` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass`
`isIntegral_algHom_iff` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `Ring.toSemiring` `AlgHom.funLike`	`IsIntegral`	—	`AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `RingHom.IsIntegralElem.map_iff` `AlgHom.comp_algebraMap_of_tower` `IsScalarTower.left`
`isIntegral_algebraMap` 📖	mathematical	—	`IsIntegral` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`RingHom.isIntegralElem_map`
`isIntegral_algebraMap_iff` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap`	`IsIntegral` `CommRing.toRing`	—	`isIntegral_algHom_iff`
`isIntegral_iff_isIntegral_closure_finite` 📖	mathematical	—	`IsIntegral` `Set.Finite` `Subring` `CommRing.toRing` `SetLike.instMembership` `Subring.instSetLike` `Subring.closure` `Subring.toCommRing` `Algebra.ofSubring`	—	`Finset.finite_toSet` `Polynomial.monic_restriction` `Polynomial.aeval_def` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `Polynomial.aeval_map_algebraMap` `Subring.instIsScalarTowerSubtypeMem` `IsScalarTower.left` `Polynomial.map_restriction` `IsIntegral.of_subring`
`isIntegral_one` 📖	mathematical	—	`IsIntegral` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`RingHom.isIntegralElem_one`
`isIntegral_zero` 📖	mathematical	—	`IsIntegral` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`RingHom.isIntegralElem_zero`
`isNoetherian_adjoin_finset` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`IsNoetherian` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `SetLike.coe` `Finset` `Finset.instSetLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Subalgebra.toCommRing` `Subalgebra.instModuleSubtypeMem`	—	`isNoetherian_of_fg_of_noetherian` `fg_adjoin_of_finite` `Finset.finite_toSet`
`map_isIntegral_int` 📖	mathematical	`IsIntegral` `Int.instCommRing` `Ring.toIntAlgebra`	`DFunLike.coe`	—	`IsIntegral.map` `AddCommGroup.intIsScalarTower` `AlgHom.algHomClass`

---

← Back to Index