Theorem IsIntegral.tmul

Modification history

2025-08-19 04:15

Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean

feat(RingTheory/IntegralClosure/Algebra/Basic): Move IsIntegral.tmul and Algebra.IsIntegral.tensorProduct (#28207) …

Modified IsIntegral.tmul View on Github →

2023-05-22 16:36

Mathlib/RingTheory/IntegralClosure.lean

feat: port RingTheory.IntegralClosure (#4196) …

Added IsIntegral.tmul View on Github →