DivisionRing

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

Statistics

Metric	Count
Definitions	0
Theorems range_smulRight_apply, range_smulRight_apply_of_surjective, surjective, surjective_iff_ne_zero	4
Total	4

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
range_smulRight_apply 📖	mathematical	—	range DivisionSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids smulRight Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.span Set Set.instSingletonSet	—	range_smulRight_apply_of_surjective surjective
range_smulRight_apply_of_surjective 📖	mathematical	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule instFunLike	range RingHomSurjective.ids smulRight IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.span Set Set.instSingletonSet	—	Submodule.ext RingHomSurjective.ids IsScalarTower.left
surjective 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule instFunLike	—	surjective_iff_ne_zero
surjective_iff_ne_zero 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule instFunLike	—	ne_zero_of_surjective GroupWithZero.toNontrivial map_smul SemilinearMapClass.toMulActionSemiHomClass semilinearMapClass inv_mul_cancel_right₀

---

← Back to Index