Equiv

📁 Source: Mathlib/Algebra/Module/Submodule/Equiv.lean

Statistics

Metric	Count
Definitions `ofBijective`, `ofEq`, `ofInjective`, `ofLeftInverse`, `ofSubmodule'`, `ofSubmodules`, `ofTop`, `codRestrictOfInjective`, `codRestrict₂`, `comap_equiv_self_of_inj_of_le`, `equivSubtypeMap`	11
Theorems `apply_ofBijective_symm_apply`, `coe_ofEq_apply`, `coe_ofTop_symm_apply`, `eq_bot_of_equiv`, `ofBijective_apply`, `ofBijective_symm_apply_apply`, `ofEq_rfl`, `ofEq_symm`, `ofInjective_apply`, `ofInjective_symm_apply`, `ofLeftInverse_apply`, `ofLeftInverse_symm_apply`, `ofSubmodule'_apply`, `ofSubmodule'_symm_apply`, `ofSubmodule'_toLinearMap`, `ofSubmodules_apply`, `ofSubmodules_symm_apply`, `ofTop_apply`, `ofTop_symm_apply`, `range`, `range_comp`, `toLinearMap_ofTop`, `codRestrictOfInjective_comp`, `codRestrictOfInjective_comp_apply`, `codRestrict₂_apply`, `comap_equiv_self_of_inj_of_le_apply`, `equivSubtypeMap_apply`, `equivSubtypeMap_symm_apply`	28
Total	39

LinearEquiv

Definitions

Name	Category	Theorems
`ofBijective` 📖	CompOp	9 math math: `DirectSum.IsInternal.ofBijective_coeLinearMap_same`, `ofBijective_symm_apply_apply`, `DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem_ne`, `ofBijective_apply`, `DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem`, `DirectSum.IsInternal.ofBijective_coeLinearMap_of_ne`, `AffineEquiv.linear_ofBijective`, `LieEquiv.ofBijective_invFun`, `apply_ofBijective_symm_apply`
`ofEq` 📖	CompOp	10 math math: `Algebra.idealMap_eq_ofEq_comp_toLocalized₀`, `AffineSubspace.linear_topEquiv`, `AffineEquiv.linear_ofEq`, `CharacterModule.intSpanEquivQuotAddOrderOf_apply`, `ContinuousLinearEquiv.toSpanNonzeroSingleton_symm_apply`, `coe_ofEq_apply`, `ofEq_symm`, `AffineSubspace.linear_equivMapOfInjective`, `ofEq_rfl`, `Module.Basis.span_neg`
`ofInjective` 📖	CompOp	6 math math: `ContinuousLinearMap.equivRange_symm_toLinearEquiv`, `ofInjective_apply`, `ContinuousLinearEquiv.toSpanNonzeroSingleton_symm_apply`, `LinearIndependent.linearCombinationEquiv_symm_apply`, `LinearMap.kerComplementEquivRange_symm_apply`, `ofInjective_symm_apply`
`ofLeftInverse` 📖	CompOp	2 math math: `ofLeftInverse_symm_apply`, `ofLeftInverse_apply`
`ofSubmodule'` 📖	CompOp	4 math math: `ofSubmodule'_symm_apply`, `ofSubmodule'_toLinearMap`, `ofSubmodule'_apply`, `Submodule.mulMap_op`
`ofSubmodules` 📖	CompOp	2 math math: `ofSubmodules_apply`, `ofSubmodules_symm_apply`
`ofTop` 📖	CompOp	7 math math: `LinearIsometryEquiv.ofTop_toLinearEquiv`, `LinearIndependent.linearCombinationEquiv_symm_apply`, `LinearMap.kerComplementEquivRange_symm_apply`, `ofTop_symm_apply`, `coe_ofTop_symm_apply`, `toLinearMap_ofTop`, `ofTop_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_ofBijective_symm_apply` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	`DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `LinearEquiv` `EquivLike.toFunLike` `instEquivLike` `symm` `ofBijective`	—	`ofBijective_apply` `apply_symm_apply`
`coe_ofEq_apply` 📖	mathematical	—	`Submodule` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule.addCommMonoid` `Submodule.module` `EquivLike.toFunLike` `instEquivLike` `ofEq`	—	`RingHomInvPair.ids`
`coe_ofTop_symm_apply` 📖	mathematical	`Top.top` `Submodule` `Submodule.instTop`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule.addCommMonoid` `Submodule.module` `EquivLike.toFunLike` `instEquivLike` `symm` `ofTop`	—	`RingHomInvPair.ids`
`eq_bot_of_equiv` 📖	mathematical	—	`Bot.bot` `Submodule` `Submodule.instBot`	—	`bot_unique` `SetLike.le_def` `instIsConcreteLE` `Submodule.mem_bot` `Submodule.mk_eq_zero` `map_eq_zero_iff` `Submodule.eq_zero_of_bot_submodule`
`ofBijective_apply` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	`DFunLike.coe` `LinearEquiv` `EquivLike.toFunLike` `instEquivLike` `ofBijective` `LinearMap` `LinearMap.instFunLike`	—	—
`ofBijective_symm_apply_apply` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	`DFunLike.coe` `LinearEquiv` `EquivLike.toFunLike` `instEquivLike` `symm` `ofBijective` `LinearMap` `LinearMap.instFunLike`	—	—
`ofEq_rfl` 📖	mathematical	—	`ofEq` `Submodule` `refl` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	`ext` `RingHomInvPair.ids`
`ofEq_symm` 📖	mathematical	—	`symm` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ofEq`	—	`RingHomInvPair.ids`
`ofInjective_apply` 📖	mathematical	`DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.range` `RingHomSurjective.invPair` `DFunLike.coe` `LinearEquiv` `Submodule.addCommMonoid` `Submodule.module` `EquivLike.toFunLike` `instEquivLike` `ofInjective` `LinearMap` `LinearMap.instFunLike`	—	`RingHomSurjective.invPair`
`ofInjective_symm_apply` 📖	mathematical	`DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	`DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `LinearEquiv` `Submodule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.range` `RingHomSurjective.invPair` `Submodule.addCommMonoid` `Submodule.module` `EquivLike.toFunLike` `instEquivLike` `symm` `ofInjective`	—	`RingHomSurjective.invPair` `LinearMap.mem_range_self` `symm_apply_apply`
`ofLeftInverse_apply` 📖	mathematical	`DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.range` `RingHomSurjective.invPair` `DFunLike.coe` `LinearEquiv` `Submodule.addCommMonoid` `Submodule.module` `EquivLike.toFunLike` `instEquivLike` `ofLeftInverse` `LinearMap` `LinearMap.instFunLike`	—	`RingHomSurjective.invPair`
`ofLeftInverse_symm_apply` 📖	mathematical	`DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	`DFunLike.coe` `LinearEquiv` `Submodule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.range` `RingHomSurjective.invPair` `Submodule.addCommMonoid` `Submodule.module` `EquivLike.toFunLike` `instEquivLike` `symm` `ofLeftInverse` `LinearMap` `LinearMap.instFunLike`	—	`RingHomSurjective.invPair`
`ofSubmodule'_apply` 📖	mathematical	—	`Submodule` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `LinearEquiv` `Submodule.comap` `toLinearMap` `Submodule.addCommMonoid` `Submodule.module` `EquivLike.toFunLike` `instEquivLike` `ofSubmodule'`	—	—
`ofSubmodule'_symm_apply` 📖	mathematical	—	`Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.comap` `toLinearMap` `DFunLike.coe` `LinearEquiv` `Submodule.addCommMonoid` `Submodule.module` `EquivLike.toFunLike` `instEquivLike` `symm` `ofSubmodule'`	—	—
`ofSubmodule'_toLinearMap` 📖	mathematical	—	`toLinearMap` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.comap` `Submodule.addCommMonoid` `Submodule.module` `ofSubmodule'` `LinearMap.codRestrict` `LinearMap.domRestrict` `Subtype.prop`	—	`LinearMap.ext` `Subtype.prop`
`ofSubmodules_apply` 📖	mathematical	`Submodule.map` `RingHomSurjective.invPair` `toLinearMap`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `LinearEquiv` `Submodule.addCommMonoid` `Submodule.module` `EquivLike.toFunLike` `instEquivLike` `ofSubmodules`	—	`RingHomSurjective.invPair`
`ofSubmodules_symm_apply` 📖	mathematical	`Submodule.map` `RingHomSurjective.invPair` `toLinearMap`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `LinearEquiv` `Submodule.addCommMonoid` `Submodule.module` `EquivLike.toFunLike` `instEquivLike` `symm` `ofSubmodules`	—	`RingHomSurjective.invPair`
`ofTop_apply` 📖	mathematical	`Top.top` `Submodule` `Submodule.instTop`	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `EquivLike.toFunLike` `instEquivLike` `ofTop`	—	`RingHomInvPair.ids`
`ofTop_symm_apply` 📖	mathematical	`Top.top` `Submodule` `Submodule.instTop`	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `EquivLike.toFunLike` `instEquivLike` `symm` `ofTop` `Top.top` `Submodule.instTop`	—	`RingHomInvPair.ids`
`range` 📖	mathematical	—	`LinearMap.range` `RingHomSurjective.invPair` `toLinearMap` `Top.top` `Submodule` `Submodule.instTop`	—	`RingHomSurjective.invPair` `LinearMap.range_eq_top` `Equiv.surjective`
`range_comp` 📖	mathematical	—	`LinearMap.range` `LinearMap.comp` `toLinearMap`	—	`LinearMap.range_comp_of_range_eq_top` `RingHomSurjective.invPair` `range`
`toLinearMap_ofTop` 📖	mathematical	`Top.top` `Submodule` `Submodule.instTop`	`toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `ofTop` `Submodule.subtype`	—	`RingHomInvPair.ids`

LinearMap

Definitions

Name	Category	Theorems
`codRestrictOfInjective` 📖	CompOp	2 math math: `codRestrictOfInjective_comp_apply`, `codRestrictOfInjective_comp`
`codRestrict₂` 📖	CompOp	1 math math: `codRestrict₂_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`codRestrictOfInjective_comp` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike` `Submodule` `SetLike.instMembership` `Submodule.setLike` `range` `RingHomSurjective.ids`	`comp` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `codRestrictOfInjective`	—	`RingHomSurjective.ids` `ext` `RingHomCompTriple.ids` `codRestrictOfInjective_comp_apply`
`codRestrictOfInjective_comp_apply` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike` `Submodule` `SetLike.instMembership` `Submodule.setLike` `range` `RingHomSurjective.ids`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike` `codRestrictOfInjective`	—	`RingHomSurjective.ids` `LinearEquiv.ofInjective_symm_apply`
`codRestrict₂_apply` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike` `Submodule` `SetLike.instMembership` `Submodule.setLike` `range` `RingHomSurjective.ids` `addCommMonoid` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike` `addCommMonoid` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `codRestrict₂`	—	`smulCommClass_self` `RingHomSurjective.ids` `LinearEquiv.ofInjective_symm_apply`

Submodule

Definitions

Name	Category	Theorems
`comap_equiv_self_of_inj_of_le` 📖	CompOp	1 math math: `comap_equiv_self_of_inj_of_le_apply`
`equivSubtypeMap` 📖	CompOp	2 math math: `equivSubtypeMap_symm_apply`, `equivSubtypeMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_equiv_self_of_inj_of_le_apply` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `LinearMap.range` `RingHomSurjective.ids`	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `SetLike.instMembership` `setLike` `comap` `addCommMonoid` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `comap_equiv_self_of_inj_of_le` `LinearMap` `LinearMap.instFunLike` `LinearMap.codRestrict` `LinearMap.comp` `subtype`	—	`RingHomSurjective.ids` `RingHomInvPair.ids`
`equivSubtypeMap_apply` 📖	mathematical	—	`Submodule` `SetLike.instMembership` `setLike` `map` `addCommMonoid` `module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `subtype` `DFunLike.coe` `LinearEquiv` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `equivSubtypeMap` `LinearMap` `LinearMap.instFunLike` `LinearMap.domRestrict`	—	`RingHomSurjective.ids` `RingHomInvPair.ids`
`equivSubtypeMap_symm_apply` 📖	mathematical	—	`Submodule` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `map` `RingHomSurjective.ids` `subtype` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `equivSubtypeMap`	—	`RingHomSurjective.ids` `RingHomInvPair.ids`

---

← Back to Index