FiniteSpan

Statistics

Metric	Count
Definitions	0
Theorems `isOfFinOrder_of_finite_of_span_eq_top_of_mapsTo`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`isOfFinOrder_of_finite_of_span_eq_top_of_mapsTo` 📖	mathematical	`Submodule.span` `Top.top` `Submodule` `Submodule.instTop` `Set.MapsTo` `DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `instEquivLike`	`IsOfFinOrder` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `automorphismGroup`	—	`RingHomInvPair.ids` `Set.Finite.injOn_iff_bijOn_of_mapsTo` `Function.Injective.injOn` `injective` `Set.finite_coe_iff` `isOfFinOrder_of_finite` `Equiv.finite_left` `ext` `Submodule.mem_top` `mul_left_iterate` `mul_one` `Submodule.span_induction` `pow_apply` `Set.MapsTo.coe_iterate_restrict` `Equiv.congr_fun` `Equiv.Perm.coe_pow` `Equiv.Perm.coe_one` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `instSemilinearEquivClass` `map_add` `SemilinearMapClass.toAddHomClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass`

---