Cardinality

📁 Source: Mathlib/RingTheory/Finiteness/Cardinality.lean

Statistics

Metric	Count
Definitions kerRepr, kerReprₛ, repr, reprEquiv, reprEquivₛ, reprₛ	6
Theorems fg_iff_exists_fin_addMonoidHom, fg_iff_exists_fin_addMonoidHom, exists_fin', exists_fin_quot_equiv, finite_basis, finite_iff_finite, finite_of_finite, not_finite_of_infinite_basis, submoduleSpan, fg_iff_exists_fin_linearMap	10
Total	16

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fg_iff_exists_fin_addMonoidHom 📖	mathematical	—	FG AddCommGroup.toAddGroup AddMonoidHom.range Pi.addGroup Int.instAddGroup	—	toIntSubmodule_toAddSubgroup Submodule.fg_iff_addSubgroup_fg RingHomSurjective.ids Submodule.fg_iff_exists_fin_linearMap DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass LinearMap.range_toAddSubgroup

AddSubmonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fg_iff_exists_fin_addMonoidHom 📖	mathematical	—	FG AddCommMonoid.toAddMonoid AddMonoidHom.mrange Pi.addZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidHom AddZeroClass.toAddZero AddMonoidHom.instFunLike AddMonoidHom.instAddMonoidHomClass	—	AddMonoidHom.instAddMonoidHomClass toNatSubmodule_toAddSubmonoid Submodule.fg_iff_addSubmonoid_fg RingHomSurjective.ids Submodule.fg_iff_exists_fin_linearMap DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass LinearMap.range_toAddSubmonoid

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_iff_finite 📖	mathematical	—	Finite Finite	—	finite_of_finite Finite.of_finite
finite_of_finite 📖	mathematical	—	Finite	—	Finite.exists_fin' Finite.of_surjective Pi.finite Finite.of_fintype
not_finite_of_infinite_basis 📖	mathematical	—	Finite	—	Finite.not_infinite Finite.finite_basis

Module.Finite

Definitions

Name	Category	Theorems
kerRepr 📖	CompOp	—
kerReprₛ 📖	CompOp	1 math math: instInvertibleReprₛ
repr 📖	CompOp	—
reprEquiv 📖	CompOp	—
reprEquivₛ 📖	CompOp	—
reprₛ 📖	CompOp	1 math math: instInvertibleReprₛ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_fin' 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike	—	RingHomSurjective.ids Submodule.fg_iff_exists_fin_linearMap fg_top LinearMap.range_eq_top
exists_fin_quot_equiv 📖	mathematical	—	LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Submodule Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Pi.Function.module Semiring.toModule Submodule.hasQuotient Pi.addCommGroup Ring.toAddCommGroup AddCommGroup.toAddCommMonoid Submodule.Quotient.addCommGroup Submodule.Quotient.module	—	RingHomInvPair.ids exists_fin'
finite_basis 📖	mathematical	—	Finite	—	basis_finite_of_finite_spans Finset.finite_toSet

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
submoduleSpan 📖	mathematical	—	Set.Finite SetLike.coe Submodule Submodule.setLike Submodule.span	—	CanLift.prf Set.instCanLiftFinsetCoeFinite eq_1 Submodule.addSubmonoidClass Submodule.smulMemClass Module.finite_iff_finite Module.Finite.span_finset

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fg_iff_exists_fin_linearMap 📖	mathematical	—	FG LinearMap.range Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule RingHom.id RingHomSurjective.ids	—	RingHomSurjective.ids AddMonoid.nat_smulCommClass' RingHomInvPair.ids Finite.of_fintype LinearEquiv.left_inv LinearEquiv.right_inv Equiv.exists_congr_right Module.Basis.constr_range

---

← Back to Index