Theorems · Theorem · commutative algebra

IsBaseChange.of_fintype_basis

∀ {R : Type u_1} [inst : CommSemiring R] {V : Type u_2} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] (A : Type u_3)
  [inst_3 : CommSemiring A] [inst_4 : Algebra A R] [inst_5 : Module A V] [inst_6 : IsScalarTower A R V] {ι : Type u_4}
  (b : Module.Basis ι R V) [inst_7 : Fintype ι], IsBaseChange R (Fintype.linearCombination A ⇑b)

Any finite basis of a module can express it as the base change of a finite free module from any under-ring.

Defined in

Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleCommSemiringAlgebraModuleIsScalarTowerFintype