Integral

📁 Source: Mathlib/RingTheory/RingHom/Integral.lean

Statistics

Metric	Count
Definitions	0
Theorems isIntegral_isStableUnderBaseChange, isIntegral_ofLocalizationSpan, isIntegral_respectsIso, isIntegral_stableUnderComposition	4
Total	4

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIntegral_isStableUnderBaseChange 📖	mathematical	—	IsStableUnderBaseChange IsIntegral CommRing.toRing	—	isIntegral_respectsIso Algebra.to_smulCommClass algebraMap_isIntegral_iff Algebra.IsIntegral.tensorProduct
isIntegral_ofLocalizationSpan 📖	mathematical	—	OfLocalizationSpan IsIntegral CommRing.toRing	—	Submodule.mem_of_span_eq_top_of_smul_pow_mem IsIntegral.exists_multiple_integral_of_isLocalization Localization.isLocalization IsScalarTower.of_algebraMap_eq' IsLocalization.lift_comp IsLocalization.map_eq_zero_iff Polynomial.hom_eval₂ map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass instRingHomClass IsScalarTower.algebraMap_apply OreLocalization.instIsScalarTower IsScalarTower.right Algebra.smul_def Submonoid.smul_def IsScalarTower.algebraMap_eq Polynomial.monic_scaleRoots_iff Polynomial.scaleRoots_eval₂_mul pow_add SemigroupAction.mul_smul MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub pow_succ smul_zero map_pow Polynomial.eval₂_one mul_one MulZeroClass.zero_mul AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass Polynomial.eq_one_of_monic_natDegree_zero
isIntegral_respectsIso 📖	mathematical	—	RespectsIso IsIntegral CommRing.toRing	—	StableUnderComposition.respectsIso isIntegral_stableUnderComposition RingEquiv.apply_symm_apply isIntegralElem_map
isIntegral_stableUnderComposition 📖	mathematical	—	StableUnderComposition IsIntegral CommRing.toRing	—	IsIntegral.trans

---

← Back to Index