Theorems · Theorem · commutative algebra

algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul

∀ {A : Type u_4} (B : Type u_5) [inst : CommSemiring A] [inst_1 : CommSemiring B] [inst_2 : Algebra A B]
  [NoZeroDivisors B] [FaithfulSMul A B] {S : Submonoid A},
  S ≤ nonZeroDivisors A → Algebra.algebraMapSubmonoid B S ≤ nonZeroDivisors B

Defined in

Mathlib.RingTheory.DedekindDomain.Instances

Cited by

2 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringCommSemiringAlgebraNoZeroDivisorsFaithfulSMul