Basis

📁 Source: FLT/Mathlib/RingTheory/TensorProduct/Basis.lean

Statistics

Metric	Count
Definitions rightBaseChange	1
Theorems rightBaseChange_apply, rightBaseChange_repr, finrank_rightAlgebra	3
Total	4

Module.Basis

Definitions

Name	Category	Theorems
rightBaseChange 📖	CompOp	2 math math: rightBaseChange_apply, rightBaseChange_repr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rightBaseChange_apply 📖	mathematical	—	TensorProduct.RightActions.instModule_fLT rightBaseChange	—	rightBaseChange_repr
rightBaseChange_repr 📖	mathematical	—	TensorProduct.RightActions.instModule_fLT rightBaseChange	—	TensorProduct.RightActions.Algebra.TensorProduct.comm_apply_tmul

TensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finrank_rightAlgebra 📖	mathematical	—	RightActions.instModule_fLT	—	—

---

← Back to Index