Rat

📁 Source: Mathlib/Algebra/Module/Rat.lean

Statistics

Metric	Count
Definitions	0
Theorems of_module_nnrat, of_module_rat, nnrat, rat, cast_smul_eq_nnqsmul, cast_smul_eq_qsmul, nnrat, nnrat', rat, rat', map_nnratCast_smul, map_nnrat_smul, map_ratCast_smul, map_rat_smul, nnratCast_smul_eq, ratCast_smul_eq, subsingleton_nnrat_module, subsingleton_rat_module	18
Total	18

IsAddTorsionFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_module_nnrat 📖	mathematical	—	IsAddTorsionFree AddCommMonoid.toAddMonoid	—	Nat.cast_smul_eq_nsmul inv_smul_smul₀ NNRat.instCharZero
of_module_rat 📖	mathematical	—	IsAddTorsionFree SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	Nat.cast_smul_eq_nsmul inv_smul_smul₀ Rat.instCharZero

IsScalarTower

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nnrat 📖	mathematical	—	IsScalarTower NNRat SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommMonoid.toAddMonoid	—	map_nnrat_smul AddMonoidHom.instAddMonoidHomClass
rat 📖	mathematical	—	IsScalarTower SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Rat.monoid Module.toDistribMulAction Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring AddCommGroup.toAddCommMonoid	—	map_rat_smul AddMonoidHom.instAddMonoidHomClass

NNRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_smul_eq_nnqsmul 📖	mathematical	—	SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring MulAction.toSemigroupAction cast DivisionSemiring.toNNRatCast NNRat Semifield.toDivisionSemiring instSemifield	—	one_smul smul_assoc IsScalarTower.left mul_one smul_one_eq_cast

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_smul_eq_qsmul 📖	mathematical	—	SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring MulAction.toSemigroupAction DivisionRing.toRatCast monoid	—	one_smul smul_assoc IsScalarTower.left mul_one smul_one_eq_cast

SMulCommClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nnrat 📖	mathematical	—	SMulCommClass NNRat SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Module.toDistribMulAction	—	map_nnrat_smul AddMonoidHom.instAddMonoidHomClass
nnrat' 📖	mathematical	—	SMulCommClass NNRat SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Module.toDistribMulAction	—	symm nnrat
rat 📖	mathematical	—	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Rat.monoid Module.toDistribMulAction Rat.semiring AddCommGroup.toAddCommMonoid	—	map_rat_smul AddMonoidHom.instAddMonoidHomClass
rat' 📖	mathematical	—	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Rat.monoid Module.toDistribMulAction Rat.semiring AddCommGroup.toAddCommMonoid	—	symm rat

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_nnratCast_smul 📖	mathematical	—	DFunLike.coe SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Module.toDistribMulAction NNRat.cast DivisionSemiring.toNNRatCast	—	NNRat.cast_def div_eq_mul_inv SemigroupAction.mul_smul map_natCast_smul map_inv_natCast_smul
map_nnrat_smul 📖	mathematical	—	DFunLike.coe NNRat SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Module.toDistribMulAction	—	map_nnratCast_smul
map_ratCast_smul 📖	mathematical	—	DFunLike.coe SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid DivisionRing.toRatCast	—	Rat.cast_def div_eq_mul_inv SemigroupAction.mul_smul map_intCast_smul map_inv_natCast_smul
map_rat_smul 📖	mathematical	—	DFunLike.coe SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Rat.monoid Module.toDistribMulAction Rat.semiring AddCommGroup.toAddCommMonoid	—	map_ratCast_smul
nnratCast_smul_eq 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Module.toDistribMulAction NNRat.cast DivisionSemiring.toNNRatCast	—	map_nnratCast_smul AddMonoidHom.instAddMonoidHomClass
ratCast_smul_eq 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid DivisionRing.toRatCast	—	map_ratCast_smul AddMonoidHom.instAddMonoidHomClass
subsingleton_nnrat_module 📖	mathematical	—	Module NNRat DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield	—	Module.ext' map_nnrat_smul AddMonoidHom.instAddMonoidHomClass
subsingleton_rat_module 📖	mathematical	—	Module Rat.semiring AddCommGroup.toAddCommMonoid	—	Module.ext' map_rat_smul AddMonoidHom.instAddMonoidHomClass

---

← Back to Index