instNoZeroSMulDivisorsCyclotomicFieldOfIsFractionRing

English

If A is a domain and K is a field with A → K, the CyclotomicField/ Ring has NoZeroSMulDivisors with respect to A.

Русский

Если A — домен и есть гомоморфизм A → K, то CyclotomicRing/Field имеет NoZeroSMulDivisors по A.

LaTeX

$$$NoZeroSMulDivisors(A,(CyclotomicField\\ n\\ K))$$$

Lean4

instance [IsFractionRing A K] : NoZeroSMulDivisors A (CyclotomicField n K) :=
  by
  rw [NoZeroSMulDivisors.iff_faithfulSMul, faithfulSMul_iff_algebraMap_injective,
    IsScalarTower.algebraMap_eq A K (CyclotomicField n K)]
  exact
    (Function.Injective.comp (FaithfulSMul.algebraMap_injective K (CyclotomicField n K))
        (IsFractionRing.injective A K) :)

Похожие утверждения