Defs

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

Statistics

Metric	Count
Definitions IsIntegralElem	1
Theorems	0
Total	1

RingHom

Definitions

Name	Category	Theorems
IsIntegralElem 📖	MathDef	21 math math: IsIntegralElem.map, IsIntegralElem.sub, IsIntegralElem.add, isIntegralElem_one, IsIntegralElem.neg, Polynomial.Monic.quotient_isIntegralElem, isIntegralElem_map, IsIntegralElem.of_map, IsIntegralElem.of_comp, isIntegralElem.of_comp, IsIntegralElem.neg_iff, isIntegralElem_leadingCoeff_mul, IsIntegralElem.of_mem_closure, IsIntegralElem.mul, IsIntegralElem.map_iff, IsIntegral.of_mem_closure'', isIntegralElem_localization_at_leadingCoeff, isIntegralElem_zero, IsIntegralElem.of_mul_unit, is_integral_localization_at_leadingCoeff, IsIntegralElem.of_neg

---

← Back to Index