holdsForLocalizationAway

Mathlib.RingTheory.RingHom.Flat

URI: https://scilib.ai/kg/mathlib#RingHom.Flat.holdsForLocalizationAway

Lean4

theorem holdsForLocalizationAway : HoldsForLocalizationAway Flat :=
  by
  introv R h
  suffices Module.Flat R S by rw [RingHom.Flat]; convert this; ext; simp_rw [Algebra.smul_def]; rfl
  exact IsLocalization.flat _ (Submonoid.powers r)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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