Namespace AdjoinRoot 10 theorems
- Quadratic algebras with unit discriminant over reduced rings
AdjoinRoot.isReduced_of_isReduced_of_isUnit_sq_sub_four_mul0 below · cited by 2 · depth 25 - The model étale local algebra R[X]/(f) over a complete local ring
AdjoinRoot.exists_isLocalRing_etale_residueField_algEquiv_of_isAdicComplete1 below · cited by 5 · depth 26 - Finite étaleness of the Kummer algebra R[X]/(Xⁿ-u)
AdjoinRoot.etale_and_finite_X_pow_sub_C_of_isUnit0 below · cited by 3 · depth 29 - Cyclotomic 𝒪-algebra as a (ℤ/m)^×-cover
AdjoinRoot.exists_monoidHom_algEquiv_bijective_tensorProduct_cyclotomic_of_isUnit1 below · cited by 1 · depth 30 - Cyclotomic algebra is finite free étale when m is invertible
AdjoinRoot.finite_free_faithfullyFlat_etale_cyclotomic_of_isUnit0 below · cited by 2 · depth 30 - Units 1-x^j in 𝒪[X]/(Φ_m) when m is invertible
AdjoinRoot.isUnit_one_sub_root_pow_of_isUnit_of_not_dvd0 below · cited by 3 · depth 30 - R[X]/(f) is a normal domain when f' is a unit
AdjoinRoot.isDomain_and_isIntegrallyClosed_of_isUnit_derivative0 below · cited by 1 · depth 32 - Adjoining a root with irreducible reduction over a local ring
AdjoinRoot.exists_isLocalRing_faithfullyFlat_residueField_algEquiv_of_irreducible_map0 below · cited by 2 · depth 34 - Functor of points of AdjoinRoot g, naturally in the test algebra
AdjoinRoot.exists_algHom_equiv_subtype_eval_map_eq_zero_natural0 below · cited by 2 · depth 38 - Adjoining a root of a distinguished monic polynomial
AdjoinRoot.exists_isLocalRing_isAdicComplete_of_monic_of_coeff_mem_maximalIdeal1 below · cited by 4 · depth 38