Int

Statistics

Metric	Count
Definitions `euclideanDomain`	1
Theorems	0
Total	1

Name	Category	Theorems
`euclideanDomain` 📖	CompOp	25 math math: `Rat.isFractionRingDen`, `AbsoluteValue.abs_isEuclidean`, `radical_eq_one_iff`, `Rat.associated_num_den`, `two_le_radical_iff`, `UniqueFactorizationMonoid.primeFactors_eq_primeFactors_natAbs`, `radical_natCast`, `Ideal.relNorm_int`, `absNorm_under_mem`, `radical_pos`, `NumberField.absNorm_differentIdeal`, `Rat.isFractionRingNum`, `absNorm_under_dvd_absNorm`, `radical_le_one_iff`, `radical_eq_prod_primeFactors`, `one_lt_radical_iff`, `radical_natAbs_eq_radical`, `ideal_span_absNorm_eq_self`, `absNorm_under_eq_sInf`, `natAbs_euclideanDomain_gcd`, `cast_mem_ideal_iff`, `Ideal.ringChar_quot`, `liesOver_span_absNorm`, `NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply`, `Nat.absNorm_under_prime`

---