Rat

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

Statistics

Metric	Count
Definitions toRatLinearMap	1
Theorems coe_toRatLinearMap, toRatLinearMap_injective	2
Total	3

AddMonoidHom

Definitions

Name	Category	Theorems
toRatLinearMap 📖	CompOp	2 math math: toRatLinearMap_injective, coe_toRatLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toRatLinearMap 📖	mathematical	—	DFunLike.coe LinearMap Rat.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike toRatLinearMap AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instFunLike	—	—
toRatLinearMap_injective 📖	mathematical	—	AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LinearMap Rat.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid toRatLinearMap	—	ext LinearMap.congr_fun

---

← Back to Index