Basic

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

Statistics

Metric	Count
Definitions `instInhabitedSubtypeFG`, `instSemilatticeSupSubtypeFG`	2
Theorems `comp`, `id`, `of_comp_finite`, `of_surjective`, `fg_top`, `finite_iff_of_bijective`, `finite_shrink`, `bot`, `equiv`, `equiv_iff`, `iff_fg`, `instIsCoatomicSubmodule`, `instMulOpposite`, `map`, `of_equiv_equiv`, `of_fg`, `of_finite`, `of_pi`, `of_restrictScalars_finite`, `of_surjective`, `pi`, `pi_iff`, `quotient`, `range`, `self`, `span_finset`, `span_of_finite`, `span_singleton`, `top`, `trans`, `ulift`, `finite`, `comp`, `id`, `of_comp_finite`, `of_surjective`, `map`, `of_finite`, `of_restrictScalars`, `restrictScalars`, `restrictScalars_iff`, `restrictScalars_of_surjective`, `span`, `stabilizes_of_iSup_eq`, `sup`, `fg_biSup`, `fg_bot`, `fg_finset_sup`, `fg_iSup`, `fg_iff_compact`, `fg_induction`, `fg_map_iff`, `fg_of_fg_map`, `fg_of_fg_map_injective`, `fg_of_linearEquiv`, `fg_pi`, `fg_range`, `fg_restrictScalars`, `fg_span`, `fg_span_singleton`, `fg_top`, `finite_finset_sup`, `finite_sup`, `instModuleFinite`	64
Total	66

AlgHom.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`AlgHom.Finite` `AlgHom.comp` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`RingHom.Finite.comp`
`id` 📖	mathematical	—	`AlgHom.Finite` `AlgHom.id` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`RingHom.Finite.id`
`of_comp_finite` 📖	mathematical	—	`AlgHom.Finite`	—	`RingHom.Finite.of_comp_finite`
`of_surjective` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike`	`AlgHom.Finite`	—	`RingHom.Finite.of_surjective`

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg_top` 📖	mathematical	—	`FG` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`Finset.coe_singleton` `span_singleton_one`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_iff_of_bijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `LinearMap` `instFunLike`	`Module.Finite`	—	`Module.Finite.of_surjective` `Function.Bijective.surjective` `Submodule.fg_of_fg_map_injective` `Function.Bijective.injective` `Submodule.map_top` `range_eq_top` `Module.finite_def`

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot` 📖	mathematical	—	`Module.Finite` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Bot.bot` `Submodule.instBot` `Submodule.addCommMonoid` `Submodule.module`	—	`of_fg` `Submodule.fg_bot`
`equiv` 📖	mathematical	—	`Module.Finite`	—	`RingHomInvPair.ids` `of_surjective` `RingHomSurjective.ids` `LinearEquiv.surjective`
`equiv_iff` 📖	mathematical	—	`Module.Finite`	—	`RingHomInvPair.ids` `equiv`
`iff_fg` 📖	mathematical	—	`Module.Finite` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `Submodule.FG`	—	`Module.finite_def` `Submodule.fg_top`
`instIsCoatomicSubmodule` 📖	mathematical	—	`IsCoatomic` `Submodule` `Submodule.instPartialOrder` `Submodule.instOrderTop`	—	`CompleteLattice.coatomic_of_top_compact` `Submodule.fg_iff_compact` `Module.finite_def`
`instMulOpposite` 📖	mathematical	—	`Module.Finite` `MulOpposite` `MulOpposite.instAddCommMonoid` `MulOpposite.instModule`	—	`equiv`
`map` 📖	mathematical	—	`Module.Finite` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.map` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.addCommMonoid` `Submodule.module`	—	`of_surjective` `RingHomSurjective.ids` `Submodule.mem_map_of_mem`
`of_equiv_equiv` 📖	mathematical	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `algebraMap` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`	`Module.Finite` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingEquiv.map_mul'` `RingEquiv.map_add'` `RingEquiv.apply_symm_apply` `DFunLike.congr_fun` `equiv` `of_restrictScalars_finite` `IsScalarTower.of_algebraMap_eq` `RingEquiv.symm_apply_apply`
`of_fg` 📖	mathematical	`Submodule.FG`	`Module.Finite` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	`iff_fg`
`of_finite` 📖	mathematical	—	`Module.Finite`	—	`nonempty_fintype` `Finset.coe_univ` `Submodule.span_univ`
`of_pi` 📖	mathematical	—	`Module.Finite`	—	`of_surjective` `RingHomSurjective.ids` `LinearMap.proj_surjective`
`of_restrictScalars_finite` 📖	mathematical	—	`Module.Finite`	—	`Module.finite_def` `Submodule.fg_def` `eq_top_iff` `Submodule.span_le_restrictScalars`
`of_surjective` 📖	mathematical	`DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	`Module.Finite`	—	`LinearMap.range_eq_top` `Submodule.map_top` `Submodule.FG.map` `fg_top`
`pi` 📖	mathematical	`Module.Finite`	`Pi.addCommMonoid` `Pi.module`	—	`Submodule.pi_top` `Submodule.fg_pi` `fg_top`
`pi_iff` 📖	mathematical	—	`Module.Finite` `Pi.addCommMonoid` `Pi.module`	—	`of_pi` `pi`
`quotient` 📖	mathematical	—	`Module.Finite` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module'`	—	`of_surjective` `RingHomSurjective.ids` `LinearMap.IsScalarTower.compatibleSMul` `Submodule.Quotient.isScalarTower` `Submodule.mkQ_surjective`
`range` 📖	mathematical	—	`Module.Finite` `Submodule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.addCommMonoid` `Submodule.module`	—	`of_surjective` `RingHomSurjective.ids` `LinearMap.semilinearMapClass`
`self` 📖	mathematical	—	`Module.Finite` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`Ideal.fg_top`
`span_finset` 📖	mathematical	—	`Module.Finite` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `SetLike.coe` `Finset` `Finset.instSetLike` `Submodule.addCommMonoid` `Submodule.module`	—	`of_fg`
`span_of_finite` 📖	mathematical	—	`Module.Finite` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Submodule.addCommMonoid` `Submodule.module`	—	`of_fg` `Set.Finite.coe_toFinset`
`span_singleton` 📖	mathematical	—	`Module.Finite` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set` `Set.instSingletonSet` `Submodule.addCommMonoid` `Submodule.module`	—	`span_of_finite` `Set.finite_singleton`
`top` 📖	mathematical	—	`Module.Finite` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Top.top` `Submodule.instTop` `Submodule.addCommMonoid` `Submodule.module`	—	`of_fg` `fg_top`
`trans` 📖	mathematical	—	`Module.Finite`	—	`Submodule.fg_def` `Set.Finite.image2` `Finset.finite_toSet` `Set.image2_smul` `Submodule.span_smul_of_span_eq_top` `Submodule.restrictScalars_top`
`ulift` 📖	mathematical	—	`Module.Finite` `ULift.addCommMonoid` `ULift.module'`	—	`equiv` `RingHomInvPair.ids`

Module.Finite.Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_shrink` 📖	mathematical	—	`Module.Finite` `Shrink` `Shrink.instAddCommMonoid` `Shrink.instModule`	—	`Module.Finite.equiv` `RingHomInvPair.ids`

RingEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite` 📖	mathematical	—	`RingHom.Finite` `toRingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`RingHom.Finite.of_surjective` `surjective`

RingHom.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`RingHom.Finite` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`IsScalarTower.of_algebraMap_eq'` `Module.Finite.trans`
`id` 📖	mathematical	—	`RingHom.Finite` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Module.Finite.self`
`of_comp_finite` 📖	mathematical	—	`RingHom.Finite`	—	`IsScalarTower.of_algebraMap_eq'` `Module.Finite.of_restrictScalars_finite`
`of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	`RingHom.Finite`	—	`Module.Finite.of_surjective` `RingHomSurjective.ids` `Module.Finite.self`

Submodule

Definitions

Name	Category	Theorems
`instInhabitedSubtypeFG` 📖	CompOp	—
`instSemilatticeSupSubtypeFG` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg_biSup` 📖	mathematical	`FG`	`iSup` `Submodule` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `Finset` `Finset.instMembership`	—	`Finset.sup_eq_iSup` `fg_finset_sup`
`fg_bot` 📖	mathematical	—	`FG` `Bot.bot` `Submodule` `instBot`	—	`Finset.coe_empty` `span_empty`
`fg_finset_sup` 📖	mathematical	`FG`	`Finset.sup` `Submodule` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `instOrderBot`	—	`Finset.sup_induction` `fg_bot` `FG.sup`
`fg_iSup` 📖	mathematical	`FG`	`iSup` `Submodule` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice`	—	`nonempty_fintype` `instFinitePLift` `iSup_congr_Prop` `iSup_pos` `iSup_plift_down` `fg_biSup`
`fg_iff_compact` 📖	mathematical	—	`FG` `IsCompactElement` `Submodule` `instPartialOrder`	—	`span_eq_iSup_of_singleton_spans` `Finset.sup_eq_iSup` `CompleteLattice.isCompactElement_finsetSup` `singleton_span_isCompactElement` `sSup_eq_iSup` `iSup_image` `span_eq` `CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup` `le_of_eq` `Finset.sup_id_eq_sSup` `sSup_le_sSup` `le_antisymm` `Finset.subset_set_image_iff` `Finset.sup_image`
`fg_induction` 📖	—	`span` `Set` `Set.instSingletonSet` `Submodule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `FG`	—	—	`Finset.induction` `Finset.coe_empty` `span_empty` `span_zero_singleton` `Finset.coe_insert` `span_insert`
`fg_map_iff` 📖	mathematical	`DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	`FG` `map`	—	`fg_of_fg_map_injective` `FG.map`
`fg_of_fg_map` 📖	—	`LinearMap.ker` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `Bot.bot` `Submodule` `instBot` `FG` `map` `RingHomSurjective.ids`	—	—	`RingHomSurjective.ids` `fg_of_fg_map_injective` `LinearMap.ker_eq_bot`
`fg_of_fg_map_injective` 📖	—	`DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `FG` `map`	—	—	`map_injective_of_injective` `map_span` `Finset.coe_preimage` `Set.image_preimage_eq_inter_range` `Set.inter_eq_self_of_subset_left` `LinearMap.coe_range` `span_le` `map_top` `map_mono` `le_top`
`fg_of_linearEquiv` 📖	—	`FG` `Top.top` `Submodule` `instTop`	—	—	`RingHomInvPair.ids` `RingHomSurjective.invPair` `RingHomSurjective.ids` `FG.map` `map_top` `LinearEquiv.range`
`fg_pi` 📖	mathematical	`FG`	`Pi.addCommMonoid` `Pi.module` `pi` `Set.univ`	—	`Set.finite_iUnion` `Set.Finite.image` `span_iUnion` `RingHomSurjective.ids` `span_image` `map.congr_simp` `iSup_map_single`
`fg_range` 📖	mathematical	—	`FG` `LinearMap.range`	—	`LinearMap.range_eq_map` `FG.map` `Module.Finite.fg_top`
`fg_restrictScalars` 📖	mathematical	`FG` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`restrictScalars` `Algebra.toSMul`	—	`FG.restrictScalars_of_surjective`
`fg_span` 📖	mathematical	—	`FG` `span`	—	`Set.Finite.coe_toFinset`
`fg_span_singleton` 📖	mathematical	—	`FG` `span` `Set` `Set.instSingletonSet`	—	`fg_span` `Set.finite_singleton`
`fg_top` 📖	mathematical	—	`FG` `Submodule` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `Top.top` `instTop`	—	`RingHomSurjective.ids` `fg_map_iff` `Subtype.val_injective` `map_top` `range_subtype`
`finite_finset_sup` 📖	mathematical	`Module.Finite` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	`Finset.sup` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `instOrderBot`	—	`Finset.sup_induction` `Module.Finite.bot` `finite_sup`
`finite_sup` 📖	mathematical	—	`Module.Finite` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `addCommMonoid` `module`	—	`Module.Finite.iff_fg` `FG.sup`

Submodule.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map` 📖	mathematical	`Submodule.FG`	`Submodule.map`	—	`Submodule.fg_def` `Set.Finite.image` `Submodule.span_image`
`of_finite` 📖	mathematical	—	`Submodule.FG`	—	`Module.Finite.iff_fg`
`of_restrictScalars` 📖	—	`Submodule.FG` `Submodule.restrictScalars`	—	—	`Submodule.restrictScalars_injective` `le_antisymm` `Submodule.span_le` `Eq.le` `Submodule.restrictScalars_le` `Submodule.span_le_restrictScalars`
`restrictScalars` 📖	mathematical	`Submodule.FG`	`Submodule.restrictScalars` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`Module.Finite.iff_fg` `Module.Finite.trans` `Submodule.isScalarTower'` `IsScalarTower.left`
`restrictScalars_iff` 📖	mathematical	—	`Submodule.FG` `Submodule.restrictScalars` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`of_restrictScalars` `restrictScalars`
`restrictScalars_of_surjective` 📖	mathematical	`Submodule.FG` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`Submodule.restrictScalars` `Algebra.toSMul`	—	`Submodule.restrictScalars_span`
`span` 📖	mathematical	`Submodule.FG`	`Submodule.span` `SetLike.coe` `Submodule` `Submodule.setLike`	—	`Submodule.span_span_of_tower`
`stabilizes_of_iSup_eq` 📖	—	`Submodule.FG` `iSup` `Submodule` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `DFunLike.coe` `OrderHom` `Nat.instPreorder` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `OrderHom.instFunLike`	—	—	`Submodule.mem_iSup_of_chain` `Submodule.subset_span` `Subtype.prop` `le_antisymm` `Submodule.span_le` `OrderHom.monotone'` `Finset.le_sup` `Finset.mem_attach` `le_iSup`
`sup` 📖	mathematical	`Submodule.FG`	`Submodule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	—	`Submodule.fg_def` `Set.Finite.union` `Submodule.span_union`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instModuleFinite` 📖	mathematical	—	`Module.Finite` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Nonneg.semiring` `Ring.toSemiring` `IsOrderedRing.toZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toPosMulMono` `Nonneg.instModule`	—	`Module.Finite.trans` `IsOrderedRing.toZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toPosMulMono` `Nonneg.instIsScalarTower` `IsScalarTower.left`

---

← Back to Index