iff_faithfulSMul

Mathlib.Algebra.Algebra.Basic

URI: https://scilib.ai/kg/mathlib#NoZeroSMulDivisors.iff_faithfulSMul

English

Same equivalence NoZeroSMulDivisors R A ↔ FaithfulSMul R A for IsDomain A.

Русский

Та же эквивалентность NoZeroSMulDivisors R A ↔ FaithfulSMul R A при условии IsDomain A.

LaTeX

$$$\text{NoZeroSMulDivisors}\; R\; A \iff \mathrm{FaithfulSMul}\; R\; A \quad(\text{IsDomain } A).$$$

Lean4

theorem iff_faithfulSMul [IsDomain A] : NoZeroSMulDivisors R A ↔ FaithfulSMul R A :=
  ⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru