Defs

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

Statistics

Metric	Count
Definitions	0
Theorems isIntegral, isIntegral_def, isIntegral_iff, algebraMap_isIntegral_iff	4
Total	4

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIntegral_def 📖	mathematical	—	IsIntegral IsIntegral	—	—
isIntegral_iff 📖	mathematical	—	IsIntegral IsIntegral	—	—

Algebra.IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIntegral 📖	mathematical	—	IsIntegral	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_isIntegral_iff 📖	mathematical	—	RingHom.IsIntegral algebraMap CommRing.toCommSemiring Ring.toSemiring Algebra.IsIntegral	—	Algebra.isIntegral_iff

---

← Back to Index