FGBaseChange

📁 Source: Mathlib/RingTheory/Adjoin/FGBaseChange.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_fg_and_mem_baseChange	1
Total	1

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_fg_and_mem_baseChange 📖	mathematical	—	Subalgebra.FG TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule Subalgebra Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass SetLike.instMembership Subalgebra.instSetLike Subalgebra.baseChange	—	Algebra.to_smulCommClass TensorProduct.exists_finset Subalgebra.fg_adjoin_finset Subalgebra.sum_mem Subalgebra.tmul_mem_baseChange Algebra.subset_adjoin Finset.mem_image_of_mem

---

← Back to Index