Theorems · Theorem · commutative algebra

Module.Flat.isBaseChange

∀ (R : Type u) (S : Type v) (M : Type w) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [Module.Flat R M] (N : Type t) [inst_6 : AddCommMonoid N]
  [inst_7 : Module R N] [inst_8 : Module S N] [inst_9 : IsScalarTower R S N] {f : M →ₗ[R] N},
  IsBaseChange S f → Module.Flat S N

A base change of a flat module is flat.

Defined in: Mathlib.RingTheory.Flat.Stability
Cited by: 1 results in Mathlib
Foundations: Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring CommSemiring Algebra AddCommMonoid Module Module.Flat AddCommMonoid Module Module IsScalarTower

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites12

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Modulestatement and proof · cited by 20,661
RingHom.idstatement and proof · cited by 18,349
AddCommMonoidstatement and proof · cited by 12,281
Algebrastatement and proof · cited by 11,388
CommSemiringstatement and proof · cited by 10,911
LinearMapstatement and proof · cited by 10,215
IsScalarTowerstatement and proof · cited by 3,896
LinearEquiv.symmproof · cited by 1,461
Module.Flatstatement and proof · cited by 279
IsBaseChangestatement and proof · cited by 87
IsBaseChange.equivproof · cited by 27
Module.Flat.of_linearEquivproof · cited by 10

Cited by1

Results whose statement or proof uses this declaration.

Module.Flat.of_isLocalizedModuleproof · cited by 1