PicardGroup

📁 Source: Mathlib/RingTheory/PicardGroup.lean

Statistics

Metric	Count
Definitions `equivPic`, `Pic`, `AsModule`, `functor`, `instAddCommGroupAsModule`, `instCoeSortType`, `mapAlgebra`, `mapRingHom`, `mk`, `linearEquiv`, `relPic`, `submoduleAlgebra`, `submoduleAlgebraEquiv`, `tensorSubmoduleAlgebraEquiv`, `tensorSubmoduleAlgebraEquivMul`, `toAlgebra`, `algEquivOfRing`, `embAlgebra`, `leftCancelEquiv`, `linearEquiv`, `linearEquivDual`, `linearEquivOfLeftInverse`, `linearEquivOfRightInverse`, `rTensorEquiv`, `rTensorInv`, `rightCancelEquiv`, `toSubmodule`, `tensorEquivMul`, `tensorInvEquiv`, `unitsQuotEquivRelPic`, `unitsToPic`, `unitsToPicEquiv`, `instCommGroupPic`	33
Theorems `equivPic_apply`, `equivPic_symm_apply`, `ext_iff`, `instFreeAsModuleOfNat`, `instFreeOfSubsingleton`, `instSubsingletonOfFiniteMaximalSpectrum`, `instSubsingletonOfIsLocalRing`, `inv_eq_dual`, `mapAlgebra_apply`, `mapAlgebra_comp_mapAlgebra`, `mapAlgebra_mapAlgebra`, `mapAlgebra_self`, `mapAlgebra_self_apply`, `mapRingHom_algebraMap`, `mapRingHom_comp_mapRingHom`, `mapRingHom_id`, `mapRingHom_id_apply`, `mapRingHom_mapRingHom`, `mk_dual`, `mk_eq_iff`, `mk_eq_mk_iff`, `mk_eq_one`, `mk_eq_one_iff`, `mk_eq_one_iff_free`, `mk_eq_self`, `mk_self`, `mk_tensor`, `mul_eq_tensor`, `subsingleton_iff`, `subsingleton_iffₛ`, `relPic_eq_top`, `eq_top_of_mk_tensor_eq_one`, `instInvertibleSubtypeMemSubmoduleSubmoduleAlgebra`, `instSubtypeMemSubmoduleSubmoduleAlgebra`, `toAlgebra_injective`, `top_mul_submoduleAlgebra`, `algEquivOfRing_apply`, `bijective`, `bijective_curry`, `bijective_of_surjective`, `embAlgebra_injective`, `exists_linearEquiv_ideal`, `finrank_eq_one`, `free_iff_linearEquiv`, `inst`, `instDual`, `instFaithfulSMul`, `instFinite`, `instLocalizationLocalizedModule`, `instProjective`, `instTensorProduct`, `instTensorProduct_1`, `instTensorProduct_2`, `lTensor_bijective_iff`, `lTensor_injective_iff`, `lTensor_surjective_iff`, `left`, `leftCancelEquiv_comp_lTensor_comp_symm`, `leftInverse_iff_rightInverse`, `leftInverse_of_rightInverse`, `linearEquivOfLeftInverse_apply`, `linearEquivOfLeftInverse_symm_apply`, `linearEquivOfRightInverse_apply`, `linearEquivOfRightInverse_symm_apply`, `of_isLocalization`, `rTensorEquiv_apply_apply`, `rTensorEquiv_symm_apply_apply`, `rTensorInv_injective`, `rTensorInv_leftInverse`, `rTensor_bijective_iff`, `rTensor_injective_iff`, `rTensor_surjective_iff`, `rank_eq_one`, `right`, `rightCancelEquiv_comp_rTensor_comp_symm`, `rightInverse_of_leftInverse`, `tensorProductComm_eq_refl`, `tmul_comm`, `toModuleEnd_bijective`, `instInvertibleSubtypeMemVal`, `ker_unitsToPic`, `mulExact_unitsMap_spanSingleton_unitsToPic`, `mulExact_unitsToPic_mapAlgebra`, `projective_of_isUnit`, `projective_units`, `range_unitsToPic`, `unitsQuotEquivRelPic_apply_coe`, `unitsQuotEquivRelPic_symm_apply`, `unitsToPic_apply`, `instInvertibleCarrierOutModuleCatValSkeleton`, `instInvertibleCarrierOutSemimoduleCatValSkeleton`, `instInvertibleReprₛ`, `instSmallUnitsSkeletonModuleCat`, `instSmallUnitsSkeletonSemimoduleCat`, `instSubsingletonPicOfIsDomainOfNonemptyNormalizedGCDMonoid`	95
Total	128

ClassGroup

Definitions

Name	Category	Theorems
`equivPic` 📖	CompOp	2 math math: `equivPic_symm_apply`, `equivPic_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivPic_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `ClassGroup` `CommRing.Pic` `CommRing.toCommSemiring` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroupClassGroup` `instCommGroupPic` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `equivPic` `Set` `Set.instMembership` `Set.range` `Units` `Submodule` `FractionRing` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `OreLocalization.instCommSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `Algebra.toModule` `OreLocalization.instAlgebra` `Algebra.id` `MonoidWithZero.toMonoid` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `MonoidHom` `Units.instGroup` `MonoidHom.instFunLike` `Submodule.unitsToPic` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `MonoidHom.ker` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.range` `QuotientGroup.Quotient.group` `Subgroup.mul` `QuotientGroup.quotientKerEquivRange` `Units.map` `MonoidWithZeroHom.toMonoidHom` `NonAssocSemiring.toMulZeroOneClass` `Submodule.spanSingleton` `QuotientGroup.congr` `MulEquiv.refl` `OreLocalization.instAddCommMonoidOreLocalization` `CommMonoid.toMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Semiring.toModule` `OreLocalization.instModuleOfIsScalarTower` `OreLocalization.instSemiring` `OreLocalization.instMonoid` `mulEquivUnitsSubmoduleQuotRange`	—	`instSmallUnitsSkeletonSemimoduleCat`
`equivPic_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `CommRing.Pic` `CommRing.toCommSemiring` `ClassGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroupPic` `instCommGroupClassGroup` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `equivPic` `HasQuotient.Quotient` `Units` `Submodule` `FractionRing` `CommSemiring.toSemiring` `OreLocalization.instAddCommMonoidOreLocalization` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `nonZeroDivisors` `Semiring.toMonoidWithZero` `OreLocalization.oreSetComm` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Semiring.toModule` `OreLocalization.instModuleOfIsScalarTower` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MonoidWithZero.toMonoid` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `OreLocalization.instSemiring` `OreLocalization.instAlgebra` `Algebra.id` `Subgroup` `Units.instGroup` `QuotientGroup.instHasQuotientSubgroup` `MonoidHom.range` `OreLocalization.instMonoid` `Units.map` `MonoidWithZeroHom.toMonoidHom` `Algebra.toModule` `NonAssocSemiring.toMulZeroOneClass` `Submodule.spanSingleton` `IsScalarTower.right` `QuotientGroup.Quotient.group` `Subgroup.normal_of_comm` `Units.instCommGroupUnits` `CommSemiring.toCommMonoid` `IdemCommSemiring.toCommSemiring` `Submodule.instIdemCommSemiring` `OreLocalization.instCommSemiring` `mulEquivUnitsSubmoduleQuotRange` `MonoidHom.ker` `Submodule.unitsToPic` `QuotientGroup.congr` `MulEquiv.refl` `Subgroup.map` `MonoidHomClass.toMonoidHom` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `Subgroup.map_symm_eq_iff_map_eq` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.mul` `QuotientGroup.quotientKerEquivRange` `CommRing.relPic` `MulEquiv.subgroupCongr` `Submodule.range_unitsToPic` `Top.top` `Subgroup.instTop` `Subgroup.topEquiv`	—	—

CommRing

Definitions

Name	Category	Theorems
`Pic` 📖	CompOp	33 math math: `Pic.mk_dual`, `Pic.instSubsingletonOfFiniteMaximalSpectrum`, `Pic.mapAlgebra_self`, `Pic.mul_eq_tensor`, `Pic.instSubsingletonOfIsLocalRing`, `Submodule.ker_unitsToPic`, `Pic.mk_tensor`, `Pic.mapRingHom_id_apply`, `relPic_eq_top`, `Pic.mk_eq_one`, `Pic.inv_eq_dual`, `Pic.subsingleton_iff`, `Pic.mapAlgebra_apply`, `Pic.mk_eq_one_iff`, `Pic.instFreeAsModuleOfNat`, `Pic.mapAlgebra_comp_mapAlgebra`, `Pic.mapRingHom_id`, `Pic.mapAlgebra_self_apply`, `Submodule.unitsToPic_apply`, `Submodule.range_unitsToPic`, `Submodule.unitsQuotEquivRelPic_symm_apply`, `Pic.mapRingHom_mapRingHom`, `ClassGroup.equivPic_symm_apply`, `Pic.mk_eq_one_iff_free`, `Pic.mapRingHom_comp_mapRingHom`, `Submodule.mulExact_unitsMap_spanSingleton_unitsToPic`, `Pic.mk_self`, `ClassGroup.equivPic_apply`, `Submodule.mulExact_unitsToPic_mapAlgebra`, `Pic.mapAlgebra_mapAlgebra`, `instSubsingletonPicOfIsDomainOfNonemptyNormalizedGCDMonoid`, `Pic.subsingleton_iffₛ`, `Submodule.unitsQuotEquivRelPic_apply_coe`
`relPic` 📖	CompOp	5 math math: `relPic_eq_top`, `Submodule.range_unitsToPic`, `Submodule.unitsQuotEquivRelPic_symm_apply`, `ClassGroup.equivPic_symm_apply`, `Submodule.unitsQuotEquivRelPic_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`relPic_eq_top` 📖	mathematical	—	`relPic` `Top.top` `Subgroup` `Pic` `CommGroup.toGroup` `instCommGroupPic` `Subgroup.instTop`	—	`top_unique`

CommRing.Pic

Definitions

Name	Category	Theorems
`AsModule` 📖	CompOp	7 math math: `mul_eq_tensor`, `inv_eq_dual`, `mk_eq_iff`, `mk_eq_self`, `mapAlgebra_apply`, `ext_iff`, `instFreeAsModuleOfNat`
`functor` 📖	CompOp	—
`instAddCommGroupAsModule` 📖	CompOp	—
`instCoeSortType` 📖	CompOp	—
`mapAlgebra` 📖	CompOp	7 math math: `mapAlgebra_self`, `mapRingHom_algebraMap`, `mapAlgebra_apply`, `mapAlgebra_comp_mapAlgebra`, `mapAlgebra_self_apply`, `Submodule.mulExact_unitsToPic_mapAlgebra`, `mapAlgebra_mapAlgebra`
`mapRingHom` 📖	CompOp	5 math math: `mapRingHom_id_apply`, `mapRingHom_algebraMap`, `mapRingHom_id`, `mapRingHom_mapRingHom`, `mapRingHom_comp_mapRingHom`
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_iff` 📖	mathematical	—	`LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AsModule` `SemimoduleCat.isAddCommMonoid` `Quotient.out` `SemimoduleCat` `CategoryTheory.isIsomorphicSetoid` `SemimoduleCat.moduleCategory` `Units.val` `CategoryTheory.Skeleton` `CategoryTheory.Skeleton.instMonoid` `SemimoduleCat.monoidalCategory` `DFunLike.coe` `Equiv` `Shrink` `Units` `instSmallUnitsSkeletonSemimoduleCat` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink` `SemimoduleCat.isModule`	—	`RingHomInvPair.ids` `instSmallUnitsSkeletonSemimoduleCat` `instInvertibleCarrierOutSemimoduleCatValSkeleton` `mk_eq_iff` `mk_eq_self`
`instFreeAsModuleOfNat` 📖	mathematical	—	`Module.Free` `AsModule` `CommRing.Pic` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `instCommGroupPic` `CommSemiring.toSemiring` `SemimoduleCat.isAddCommMonoid` `Quotient.out` `SemimoduleCat` `CategoryTheory.isIsomorphicSetoid` `SemimoduleCat.moduleCategory` `Units.val` `CategoryTheory.Skeleton` `CategoryTheory.Skeleton.instMonoid` `SemimoduleCat.monoidalCategory` `DFunLike.coe` `Equiv` `Shrink` `Units` `instSmallUnitsSkeletonSemimoduleCat` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink` `SemimoduleCat.isModule`	—	`instSmallUnitsSkeletonSemimoduleCat` `instInvertibleCarrierOutSemimoduleCatValSkeleton` `mk_eq_one_iff_free` `mk_eq_self`
`instFreeOfSubsingleton` 📖	mathematical	—	`Module.Free` `CommSemiring.toSemiring`	—	`Module.Invertible.instFinite` `Module.Finite.exists_fin'` `subsingleton_iffₛ` `instInvertibleReprₛ` `Module.Free.of_equiv`
`instSubsingletonOfFiniteMaximalSpectrum` 📖	mathematical	—	`CommRing.Pic` `CommRing.toCommSemiring`	—	`subsingleton_iff` `Module.free_of_flat_of_finrank_eq` `Module.Invertible.instFinite` `Module.Flat.of_projective` `Module.Invertible.instProjective` `Module.Invertible.finrank_eq_one` `Algebra.to_smulCommClass` `Module.Invertible.instTensorProduct_2` `IsScalarTower.right` `Module.Invertible.inst` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `MaximalSpectrum.isMaximal` `Field.instIsLocalRing` `instFreeOfSubsingleton` `instSubsingletonOfIsLocalRing`
`instSubsingletonOfIsLocalRing` 📖	mathematical	—	`CommRing.Pic` `CommRing.toCommSemiring`	—	`subsingleton_iff` `Module.free_of_flat_of_isLocalRing` `Module.Invertible.instFinite` `Module.Flat.of_projective` `Module.Invertible.instProjective`
`inv_eq_dual` 📖	mathematical	—	`CommRing.Pic` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `instCommGroupPic` `Module.Dual` `AsModule` `CommSemiring.toSemiring` `SemimoduleCat.isAddCommMonoid` `Quotient.out` `SemimoduleCat` `CategoryTheory.isIsomorphicSetoid` `SemimoduleCat.moduleCategory` `Units.val` `CategoryTheory.Skeleton` `CategoryTheory.Skeleton.instMonoid` `SemimoduleCat.monoidalCategory` `DFunLike.coe` `Equiv` `Shrink` `Units` `instSmallUnitsSkeletonSemimoduleCat` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink` `SemimoduleCat.isModule` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `Module.Invertible.instDual` `instInvertibleCarrierOutSemimoduleCatValSkeleton`	—	`instSmallUnitsSkeletonSemimoduleCat` `Algebra.to_smulCommClass` `Module.Invertible.instDual` `instInvertibleCarrierOutSemimoduleCatValSkeleton` `mk_dual` `mk_eq_self`
`mapAlgebra_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `CommRing.Pic` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroupPic` `MonoidHom.instFunLike` `mapAlgebra` `TensorProduct` `AsModule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `SemimoduleCat.isAddCommMonoid` `Quotient.out` `SemimoduleCat` `CategoryTheory.isIsomorphicSetoid` `SemimoduleCat.moduleCategory` `Units.val` `CategoryTheory.Skeleton` `CategoryTheory.Skeleton.instMonoid` `SemimoduleCat.monoidalCategory` `Equiv` `Shrink` `Units` `instSmallUnitsSkeletonSemimoduleCat` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink` `Algebra.toModule` `SemimoduleCat.isModule` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule`	—	`instSmallUnitsSkeletonSemimoduleCat`
`mapAlgebra_comp_mapAlgebra` 📖	mathematical	—	`MonoidHom.comp` `CommRing.Pic` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroupPic` `mapAlgebra`	—	`MonoidHom.ext` `MonoidHom.comp_apply` `mapAlgebra_mapAlgebra`
`mapAlgebra_mapAlgebra` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `CommRing.Pic` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroupPic` `MonoidHom.instFunLike` `mapAlgebra`	—	`instSmallUnitsSkeletonSemimoduleCat` `Module.Invertible.instTensorProduct_2` `instInvertibleCarrierOutSemimoduleCatValSkeleton` `IsScalarTower.right` `Module.Invertible.inst` `RingHomInvPair.ids` `mk_eq_mk_iff` `IsScalarTower.to_smulCommClass` `RingHomCompTriple.ids`
`mapAlgebra_self` 📖	mathematical	—	`mapAlgebra` `Algebra.id` `MonoidHom.id` `CommRing.Pic` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroupPic`	—	`MonoidHom.ext` `mapAlgebra_self_apply`
`mapAlgebra_self_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `CommRing.Pic` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroupPic` `MonoidHom.instFunLike` `mapAlgebra` `Algebra.id`	—	`instSmallUnitsSkeletonSemimoduleCat` `Module.Invertible.instTensorProduct_2` `instInvertibleCarrierOutSemimoduleCatValSkeleton` `IsScalarTower.right` `Module.Invertible.inst` `RingHomInvPair.ids` `mk_eq_iff`
`mapRingHom_algebraMap` 📖	mathematical	—	`mapRingHom` `algebraMap` `CommSemiring.toSemiring` `mapAlgebra`	—	`mapRingHom.eq_1` `toAlgebra_algebraMap`
`mapRingHom_comp_mapRingHom` 📖	mathematical	—	`MonoidHom.comp` `CommRing.Pic` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroupPic` `mapRingHom` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`IsScalarTower.of_algebraMap_eq'` `mapAlgebra_comp_mapAlgebra`
`mapRingHom_id` 📖	mathematical	—	`mapRingHom` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MonoidHom.id` `CommRing.Pic` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroupPic`	—	`mapRingHom.eq_1` `mapAlgebra_self`
`mapRingHom_id_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `CommRing.Pic` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroupPic` `MonoidHom.instFunLike` `mapRingHom` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`mapRingHom_id`
`mapRingHom_mapRingHom` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `CommRing.Pic` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroupPic` `MonoidHom.instFunLike` `mapRingHom` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`mapRingHom_comp_mapRingHom`
`mk_dual` 📖	mathematical	—	`Module.Dual` `CommSemiring.toSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `Module.Invertible.instDual` `CommRing.Pic` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `instCommGroupPic`	—	`instSmallUnitsSkeletonSemimoduleCat` `Algebra.to_smulCommClass` `Module.Invertible.instFinite` `Module.Invertible.instDual` `Units.ext` `Equiv.symm_apply_apply` `smulCommClass_self` `Module.Finite.exists_fin'` `RingHomCompTriple.ids` `RingHomInvPair.ids`
`mk_eq_iff` 📖	mathematical	—	`LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AsModule` `SemimoduleCat.isAddCommMonoid` `Quotient.out` `SemimoduleCat` `CategoryTheory.isIsomorphicSetoid` `SemimoduleCat.moduleCategory` `Units.val` `CategoryTheory.Skeleton` `CategoryTheory.Skeleton.instMonoid` `SemimoduleCat.monoidalCategory` `DFunLike.coe` `Equiv` `Shrink` `Units` `instSmallUnitsSkeletonSemimoduleCat` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink` `SemimoduleCat.isModule`	—	`RingHomInvPair.ids` `instSmallUnitsSkeletonSemimoduleCat` `Module.Invertible.instFinite` `Equiv.apply_eq_iff_eq_symm_apply` `Units.ext` `Quotient.mk_eq_iff_out` `Module.Finite.exists_fin'` `RingHomCompTriple.ids`
`mk_eq_mk_iff` 📖	mathematical	—	`LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids`	—	`RingHomInvPair.ids` `instSmallUnitsSkeletonSemimoduleCat` `mk_eq_iff` `RingHomCompTriple.ids`
`mk_eq_one` 📖	mathematical	—	`CommRing.Pic` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `instCommGroupPic`	—	`mk_eq_one_iff_free`
`mk_eq_one_iff` 📖	mathematical	—	`CommRing.Pic` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `instCommGroupPic` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`RingHomInvPair.ids` `Module.Invertible.inst` `mk_self` `mk_eq_mk_iff`
`mk_eq_one_iff_free` 📖	mathematical	—	`CommRing.Pic` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `instCommGroupPic` `Module.Free` `CommSemiring.toSemiring`	—	`RingHomInvPair.ids` `mk_eq_one_iff` `Module.Invertible.free_iff_linearEquiv`
`mk_eq_self` 📖	mathematical	—	`AsModule` `SemimoduleCat.isAddCommMonoid` `CommSemiring.toSemiring` `Quotient.out` `SemimoduleCat` `CategoryTheory.isIsomorphicSetoid` `SemimoduleCat.moduleCategory` `Units.val` `CategoryTheory.Skeleton` `CategoryTheory.Skeleton.instMonoid` `SemimoduleCat.monoidalCategory` `DFunLike.coe` `Equiv` `Shrink` `Units` `instSmallUnitsSkeletonSemimoduleCat` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink` `SemimoduleCat.isModule` `instInvertibleCarrierOutSemimoduleCatValSkeleton`	—	`instSmallUnitsSkeletonSemimoduleCat` `instInvertibleCarrierOutSemimoduleCatValSkeleton` `RingHomInvPair.ids` `mk_eq_iff`
`mk_self` 📖	mathematical	—	`NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `Module.Invertible.inst` `CommRing.Pic` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `instCommGroupPic`	—	`instSmallUnitsSkeletonSemimoduleCat` `Module.Invertible.instFinite` `Module.Invertible.inst` `Units.ext` `Module.Finite.exists_fin'`
`mk_tensor` 📖	mathematical	—	`TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Module.Invertible.instTensorProduct_2` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `CommRing.Pic` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroupPic`	—	`instSmallUnitsSkeletonSemimoduleCat` `Module.Invertible.instFinite` `Module.Invertible.instTensorProduct_2` `IsScalarTower.left` `Units.ext` `Equiv.symm_apply_apply` `Module.Finite.exists_fin'` `RingHomCompTriple.ids` `RingHomInvPair.ids` `CategoryTheory.Skeleton.toSkeleton_tensorObj`
`mul_eq_tensor` 📖	mathematical	—	`CommRing.Pic` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroupPic` `TensorProduct` `AsModule` `SemimoduleCat.isAddCommMonoid` `CommSemiring.toSemiring` `Quotient.out` `SemimoduleCat` `CategoryTheory.isIsomorphicSetoid` `SemimoduleCat.moduleCategory` `Units.val` `CategoryTheory.Skeleton` `CategoryTheory.Skeleton.instMonoid` `SemimoduleCat.monoidalCategory` `DFunLike.coe` `Equiv` `Shrink` `Units` `instSmallUnitsSkeletonSemimoduleCat` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink` `SemimoduleCat.isModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Module.Invertible.instTensorProduct_2` `instInvertibleCarrierOutSemimoduleCatValSkeleton` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`instSmallUnitsSkeletonSemimoduleCat` `Module.Invertible.instTensorProduct_2` `instInvertibleCarrierOutSemimoduleCatValSkeleton` `IsScalarTower.left` `mk_tensor` `mk_eq_self`
`subsingleton_iff` 📖	mathematical	—	`CommRing.Pic` `CommRing.toCommSemiring` `Module.Free` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`subsingleton_iffₛ`
`subsingleton_iffₛ` 📖	mathematical	—	`CommRing.Pic` `Module.Free` `CommSemiring.toSemiring`	—	`instSmallUnitsSkeletonSemimoduleCat` `instInvertibleCarrierOutSemimoduleCatValSkeleton` `mk_eq_self` `mk_eq_one_iff_free`

CommRing.Pic.mk

Definitions

Name	Category	Theorems
`linearEquiv` 📖	CompOp	—

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_top_of_mk_tensor_eq_one` 📖	mathematical	`CommRing.toCommSemiring` `TensorProduct` `Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.addCommMonoid` `Submodule.module` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Module.Invertible.instTensorProduct_2` `Algebra.id` `Submodule.isScalarTower'` `Algebra.toSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `IsScalarTower.right` `CommRing.Pic` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `instCommGroupPic`	`Top.top` `Submodule.instTop`	—	`Module.Invertible.instTensorProduct_2` `Submodule.isScalarTower'` `IsScalarTower.right` `RingHomInvPair.ids` `CommRing.Pic.mk_eq_one_iff` `RingHomCompTriple.ids` `Submodule.LinearDisjoint.of_left_le_one_of_flat` `LE.le.trans` `le_top` `Eq.ge` `one_eq_top` `Module.Flat.of_projective` `Module.Invertible.instProjective` `IsFractionRing.self_iff_nonZeroDivisors_le_isUnit` `IsRegular.mem_nonZeroDivisors` `isRightRegular_iff_isRegular` `IsRightRegular.eq_1` `smul_eq_mul` `IsScalarTower.left` `Submodule.coe_smul` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `mul_one` `Subtype.val_injective` `LinearEquiv.injective` `eq_top_of_isUnit_mem` `mul_le_right` `instIsTwoSided_1` `mul_le_left`

Module.Flat

Definitions

Name	Category	Theorems
`submoduleAlgebra` 📖	CompOp	3 math math: `instSubtypeMemSubmoduleSubmoduleAlgebra`, `top_mul_submoduleAlgebra`, `instInvertibleSubtypeMemSubmoduleSubmoduleAlgebra`
`submoduleAlgebraEquiv` 📖	CompOp	—
`tensorSubmoduleAlgebraEquiv` 📖	CompOp	—
`tensorSubmoduleAlgebraEquivMul` 📖	CompOp	—
`toAlgebra` 📖	CompOp	2 math math: `toAlgebra_injective`, `Module.Invertible.embAlgebra_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instInvertibleSubtypeMemSubmoduleSubmoduleAlgebra` 📖	mathematical	—	`Module.Invertible` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `submoduleAlgebra` `Submodule.addCommMonoid` `Submodule.module`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `Module.Invertible.congr`
`instSubtypeMemSubmoduleSubmoduleAlgebra` 📖	mathematical	—	`Module.Flat` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `submoduleAlgebra` `Submodule.addCommMonoid` `Submodule.module`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `of_linearEquiv`
`toAlgebra_injective` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `LinearMap.instFunLike` `toAlgebra`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `EquivLike.toEmbeddingLike` `rTensor_preserves_injective_linearMap` `FaithfulSMul.algebraMap_injective`
`top_mul_submoduleAlgebra` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Submodule.mul` `IsScalarTower.right` `Top.top` `Submodule.instTop` `submoduleAlgebra`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `IsScalarTower.right` `RingHomSurjective.ids` `Submodule.mulMap_range` `RingHomSurjective.invPair` `RingHomCompTriple.ids` `LinearMap.IsScalarTower.compatibleSMul` `TensorProduct.isScalarTower_left` `TensorProduct.AlgebraTensorModule.curry_injective` `Submodule.isScalarTower'` `IsScalarTower.left` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `LinearEquiv.range`

Module.Invertible

Definitions

Name	Category	Theorems
`algEquivOfRing` 📖	CompOp	1 math math: `algEquivOfRing_apply`
`embAlgebra` 📖	CompOp	—
`leftCancelEquiv` 📖	CompOp	1 math math: `leftCancelEquiv_comp_lTensor_comp_symm`
`linearEquiv` 📖	CompOp	—
`linearEquivDual` 📖	CompOp	—
`linearEquivOfLeftInverse` 📖	CompOp	2 math math: `linearEquivOfLeftInverse_symm_apply`, `linearEquivOfLeftInverse_apply`
`linearEquivOfRightInverse` 📖	CompOp	2 math math: `linearEquivOfRightInverse_symm_apply`, `linearEquivOfRightInverse_apply`
`rTensorEquiv` 📖	CompOp	2 math math: `rTensorEquiv_apply_apply`, `rTensorEquiv_symm_apply_apply`
`rTensorInv` 📖	CompOp	2 math math: `rTensorInv_leftInverse`, `rTensorInv_injective`
`rightCancelEquiv` 📖	CompOp	2 math math: `rTensorEquiv_symm_apply_apply`, `rightCancelEquiv_comp_rTensor_comp_symm`
`toSubmodule` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algEquivOfRing_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `CommSemiring.toSemiring` `Algebra.id` `AlgEquiv.instFunLike` `algEquivOfRing` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	—
`bijective` 📖	mathematical	—	`Function.Bijective` `TensorProduct` `Module.Dual` `CommSemiring.toSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `DFunLike.coe` `LinearMap` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `contractLeft`	—	—
`bijective_curry` 📖	mathematical	—	`Function.Bijective` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.instFunLike` `TensorProduct.curry` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`RingHomInvPair.ids` `smulCommClass_self` `TensorProduct.smulCommClass_left` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap_symm_comp_eq` `LinearMap.ext` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.right` `TensorProduct.isScalarTower` `IsScalarTower.left` `LinearMap.ext_ring` `IsScalarTower.to_smulCommClass` `one_smul` `LinearEquiv.symm_apply_apply` `LinearEquiv.bijective`
`bijective_of_surjective` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`Function.Bijective`	—	`Algebra.to_smulCommClass` `RingHomCompTriple.ids` `RingHomInvPair.ids` `instDual` `instTensorProduct`
`embAlgebra_injective` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `LinearMap.instFunLike` `Module.Flat.toAlgebra`	—	`Module.Flat.toAlgebra_injective`
`exists_linearEquiv_ideal` 📖	mathematical	—	`LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `AddCommGroup.toAddCommMonoid` `Submodule.addCommMonoid` `Submodule.module`	—	`FractionRing.instFaithfulSMul` `instFaithfulSMul` `inst` `RingHomInvPair.ids` `Submodule.range_unitsToPic` `Submodule.instInvertibleSubtypeMemVal` `CommRing.Pic.mk_eq_mk_iff` `Units.submodule_isFractional` `Localization.isLocalization` `RingHomCompTriple.ids`
`finrank_eq_one` 📖	mathematical	—	`Module.finrank` `CommSemiring.toSemiring`	—	`subsingleton_or_nontrivial` `Module.rank_eq_one_iff_finrank_eq_one` `rank_subsingleton` `LinearEquiv.finrank_eq` `RingHomInvPair.ids` `free_iff_linearEquiv` `Module.finrank_self`
`free_iff_linearEquiv` 📖	mathematical	—	`Module.Free` `CommSemiring.toSemiring` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`RingHomInvPair.ids` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `instFinite` `card_eq_of_linearEquiv` `invariantBasisNumber_of_rankCondition` `rankCondition_of_nontrivial_of_commSemiring` `RingHomCompTriple.ids` `smulCommClass_self` `Finite.instProd` `Finite.of_fintype` `Algebra.to_smulCommClass` `Fintype.card_eq_one_iff_nonempty_unique` `Fintype.card_prod` `Fintype.card_unique` `Unique.instSubsingleton` `Module.Free.of_equiv` `Module.Free.self`
`inst` 📖	mathematical	—	`Module.Invertible` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule`	—	`left`
`instDual` 📖	mathematical	—	`Module.Invertible` `Module.Dual` `CommSemiring.toSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id`	—	`left` `Algebra.to_smulCommClass`
`instFaithfulSMul` 📖	mathematical	—	`FaithfulSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction`	—	`Function.Bijective.injective` `smulCommClass_self` `toModuleEnd_bijective` `LinearMap.ext`
`instFinite` 📖	mathematical	—	`Module.Finite` `CommSemiring.toSemiring`	—	—
`instLocalizationLocalizedModule` 📖	mathematical	—	`Module.Invertible` `Localization` `CommSemiring.toCommMonoid` `LocalizedModule` `OreLocalization.instCommSemiring` `OreLocalization.oreSetComm` `OreLocalization.instAddCommMonoidOreLocalization` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `OreLocalization.instModule`	—	`of_isLocalization` `IsScalarTower.left` `IsScalarTower.right` `Localization.isLocalization` `localizedModuleIsLocalizedModule` `OreLocalization.instIsScalarTower_1`
`instProjective` 📖	mathematical	—	`Module.Projective` `CommSemiring.toSemiring`	—	—
`instTensorProduct` 📖	mathematical	—	`Module.Invertible` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`right` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `RingHomInvPair.ids`
`instTensorProduct_1` 📖	mathematical	—	`Module.Invertible` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass`	—	`right` `Algebra.to_smulCommClass` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `RingHomCompTriple.ids` `RingHomInvPair.ids`
`instTensorProduct_2` 📖	mathematical	—	`Module.Invertible` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `CommSemiring.toSemiring` `IsScalarTower.to_smulCommClass`	—	`congr` `Algebra.to_smulCommClass` `smulCommClass_self` `IsScalarTower.to_smulCommClass` `instTensorProduct` `instTensorProduct_1` `IsScalarTower.left`
`lTensor_bijective_iff` 📖	mathematical	—	`Function.Bijective` `TensorProduct` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.lTensor`	—	—
`lTensor_injective_iff` 📖	mathematical	—	`TensorProduct` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.lTensor`	—	`Algebra.to_smulCommClass` `RingHomCompTriple.ids` `RingHomInvPair.ids` `leftCancelEquiv_comp_lTensor_comp_symm` `EquivLike.toEmbeddingLike` `Module.Flat.lTensor_preserves_injective_linearMap` `Module.Flat.of_projective` `Module.dual_projective` `instFinite` `instProjective`
`lTensor_surjective_iff` 📖	mathematical	—	`TensorProduct` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.lTensor`	—	`Algebra.to_smulCommClass` `RingHomCompTriple.ids` `RingHomInvPair.ids` `leftCancelEquiv_comp_lTensor_comp_symm` `LinearMap.lTensor_surjective`
`left` 📖	mathematical	—	`Module.Invertible`	—	`RingHomInvPair.ids` `right` `RingHomCompTriple.ids`
`leftCancelEquiv_comp_lTensor_comp_symm` 📖	mathematical	—	`LinearMap.comp` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `leftCancelEquiv` `LinearMap.lTensor` `LinearEquiv.symm`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `LinearMap.comp_assoc` `LinearEquiv.comp_toLinearMap_symm_eq` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`leftInverse_iff_rightInverse` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	`rightInverse_of_leftInverse` `leftInverse_of_rightInverse`
`leftInverse_of_rightInverse` 📖	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	—	`rightInverse_of_leftInverse`
`linearEquivOfLeftInverse_apply` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`LinearEquiv` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `linearEquivOfLeftInverse`	—	`RingHomInvPair.ids`
`linearEquivOfLeftInverse_symm_apply` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`LinearEquiv` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `linearEquivOfLeftInverse`	—	`RingHomInvPair.ids`
`linearEquivOfRightInverse_apply` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`LinearEquiv` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `linearEquivOfRightInverse`	—	`RingHomInvPair.ids`
`linearEquivOfRightInverse_symm_apply` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`LinearEquiv` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `linearEquivOfRightInverse`	—	`RingHomInvPair.ids`
`of_isLocalization` 📖	mathematical	—	`Module.Invertible`	—	`congr` `Algebra.to_smulCommClass` `instTensorProduct_1` `IsLocalizedModule.isBaseChange`
`rTensorEquiv_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearEquiv` `RingHomInvPair.ids` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `rTensorEquiv` `AddMonoidHom` `AddZeroClass.toAddZero` `TensorProduct.addZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `TensorProduct.liftAux` `LinearMap.comp`	—	`RingHomInvPair.ids` `LinearMap.comp.congr_simp` `LinearMap.compl₂_id`
`rTensorEquiv_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `LinearEquiv` `RingHomInvPair.ids` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.addCommMonoid` `LinearMap.module` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `rTensorEquiv` `LinearEquiv.congrRight` `rightCancelEquiv` `LinearMap.rTensor` `TensorProduct.assoc` `TensorProduct.tmul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`RingHomInvPair.ids` `TensorProduct.smulCommClass_left` `smulCommClass_self`
`rTensorInv_injective` 📖	mathematical	—	`LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `DFunLike.coe` `LinearMap.addCommMonoid` `LinearMap.module` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `LinearMap.instFunLike` `rTensorInv`	—	`RingHomInvPair.ids` `TensorProduct.smulCommClass_left` `smulCommClass_self` `EquivLike.toEmbeddingLike` `RingHomCompTriple.ids` `rTensorInv_leftInverse`
`rTensorInv_leftInverse` 📖	mathematical	—	`LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `DFunLike.coe` `LinearMap.addCommMonoid` `LinearMap.module` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `LinearMap.instFunLike` `rTensorInv` `LinearMap.rTensorHom`	—	`RingHomInvPair.ids` `TensorProduct.smulCommClass_left` `smulCommClass_self` `LinearEquiv.eq_symm_apply` `TensorProduct.AlgebraTensorModule.curry_injective` `TensorProduct.isScalarTower` `IsScalarTower.left` `IsScalarTower.to_smulCommClass` `LinearMap.instIsScalarTower` `LinearMap.ext` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`rTensor_bijective_iff` 📖	mathematical	—	`Function.Bijective` `TensorProduct` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.rTensor`	—	—
`rTensor_injective_iff` 📖	mathematical	—	`TensorProduct` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.rTensor`	—	`lTensor_injective_iff`
`rTensor_surjective_iff` 📖	mathematical	—	`TensorProduct` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.rTensor`	—	`LinearMap.lTensor_surj_iff_rTensor_surj` `lTensor_surjective_iff`
`rank_eq_one` 📖	mathematical	—	`Module.rank` `CommSemiring.toSemiring` `Cardinal` `Cardinal.instOne`	—	`Module.rank_eq_one_iff_finrank_eq_one` `finrank_eq_one`
`right` 📖	mathematical	—	`Module.Invertible`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `LinearEquiv.coe_trans` `LinearEquiv.eq_comp_toLinearMap_symm` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `IsScalarTower.right` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `LinearEquiv.bijective`
`rightCancelEquiv_comp_rTensor_comp_symm` 📖	mathematical	—	`LinearMap.comp` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `rightCancelEquiv` `LinearMap.rTensor` `LinearEquiv.symm`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `LinearMap.comp_assoc` `LinearEquiv.comp_toLinearMap_symm_eq` `TensorProduct.AlgebraTensorModule.curry_injective` `TensorProduct.isScalarTower` `IsScalarTower.left` `smulCommClass_self` `IsScalarTower.to_smulCommClass` `LinearMap.instIsScalarTower` `LinearMap.ext` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`rightInverse_of_leftInverse` 📖	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	—	`Function.Bijective.injective` `bijective_of_surjective` `Function.LeftInverse.surjective`
`tensorProductComm_eq_refl` 📖	mathematical	—	`TensorProduct.comm` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearEquiv.refl` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`Ideal.IsMaximal.isPrime'` `IsScalarTower.left` `IsScalarTower.right` `LinearEquiv.toLinearMap_injective` `RingHomInvPair.ids` `LinearMap.eq_of_localization_maximal` `IsLocalization.instIsLocalizedModuleTensorProductMap` `localizedModuleIsLocalizedModule` `smulCommClass_self` `IsLocalizedModule.linearMap_ext` `TensorProduct.AlgebraTensorModule.curry_injective` `TensorProduct.isScalarTower` `OreLocalization.instIsScalarTower` `RingHomCompTriple.ids` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `IsLocalizedModule.map_apply` `free_iff_linearEquiv` `instLocalizationLocalizedModule` `CommRing.Pic.instFreeOfSubsingleton` `CommRing.Pic.instSubsingletonOfFiniteMaximalSpectrum` `Finite.of_fintype` `Localization.AtPrime.isLocalRing` `LinearMap.IsScalarTower.compatibleSMul` `OreLocalization.instIsScalarTower_1` `LinearEquiv.injective` `IsScalarTower.to_smulCommClass'` `TensorProduct.CompatibleSMul.isScalarTower` `IsLocalization.instCompatibleSMulLocalizationOfIsScalarTower_1` `mul_one` `smul_eq_mul` `TensorProduct.smul_tmul` `mul_comm` `IsLocalizedModule.map_id`
`tmul_comm` 📖	mathematical	—	`TensorProduct.tmul` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`DFunLike.congr_fun` `RingHomInvPair.ids` `tensorProductComm_eq_refl`
`toModuleEnd_bijective` 📖	mathematical	—	`Function.Bijective` `Module.End` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Module.End.instSemiring` `RingHom.instFunLike` `Module.toModuleEnd` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`smulCommClass_self` `RingHomInvPair.ids` `TensorProduct.smulCommClass_left` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `LinearMap.ext` `rTensorEquiv_apply_apply` `one_mul` `Equiv.bijective`

Submodule

Definitions

Name	Category	Theorems
`tensorEquivMul` 📖	CompOp	—
`tensorInvEquiv` 📖	CompOp	—
`unitsQuotEquivRelPic` 📖	CompOp	2 math math: `unitsQuotEquivRelPic_symm_apply`, `unitsQuotEquivRelPic_apply_coe`
`unitsToPic` 📖	CompOp	9 math math: `ker_unitsToPic`, `unitsToPic_apply`, `range_unitsToPic`, `unitsQuotEquivRelPic_symm_apply`, `ClassGroup.equivPic_symm_apply`, `mulExact_unitsMap_spanSingleton_unitsToPic`, `ClassGroup.equivPic_apply`, `mulExact_unitsToPic_mapAlgebra`, `unitsQuotEquivRelPic_apply_coe`
`unitsToPicEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instInvertibleSubtypeMemVal` 📖	mathematical	—	`Module.Invertible` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `setLike` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `idemSemiring` `addCommMonoid` `module`	—	`Module.Invertible.left`
`ker_unitsToPic` 📖	mathematical	—	`MonoidHom.ker` `Units` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `idemSemiring` `Units.instGroup` `CommRing.Pic` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroupPic` `unitsToPic` `MonoidHom.range` `Units.map` `MonoidWithZeroHom.toMonoidHom` `NonAssocSemiring.toMulZeroOneClass` `spanSingleton`	—	`Subgroup.ext` `RingHomInvPair.ids` `instInvertibleSubtypeMemVal` `CommRing.Pic.mk_eq_one_iff` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass` `Subgroup.instSubgroupClass` `eq_span_singleton_of_surjective` `LinearEquiv.surjective` `isUnit_iff_exists_and_exists` `IsScalarTower.right` `span_mul_span` `Set.mul_singleton` `Set.image_singleton` `Units.mul_inv` `span_singleton_eq_one_iff` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Units.inv_mul` `mul_assoc` `Units.ext` `RingHomSurjective.invPair` `RingHomCompTriple.ids` `faithfulSMul_iff_injective_smul_one` `Algebra.smul_mul_assoc` `ext`
`mulExact_unitsMap_spanSingleton_unitsToPic` 📖	mathematical	—	`Function.MulExact` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `IdemSemiring.toSemiring` `idemSemiring` `CommRing.Pic` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Units.instMulOneClass` `MonoidHom.instFunLike` `Units.map` `MonoidWithZeroHom.toMonoidHom` `NonAssocSemiring.toMulZeroOneClass` `spanSingleton` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroupPic` `unitsToPic` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	—	`MonoidHom.mulExact_iff` `ker_unitsToPic`
`mulExact_unitsToPic_mapAlgebra` 📖	mathematical	—	`Function.MulExact` `Units` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `idemSemiring` `CommRing.Pic` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Units.instMulOneClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroupPic` `MonoidHom.instFunLike` `unitsToPic` `CommRing.Pic.mapAlgebra` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	—	`MonoidHom.mulExact_iff` `range_unitsToPic`
`projective_of_isUnit` 📖	mathematical	`IsUnit` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `idemSemiring`	`Module.Projective` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	—	`projective_units`
`projective_units` 📖	mathematical	—	`Module.Projective` `CommSemiring.toSemiring` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `setLike` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `idemSemiring` `addCommMonoid` `module`	—	`RingHomCompTriple.ids` `Algebra.to_smulCommClass` `IsScalarTower.right`
`range_unitsToPic` 📖	mathematical	—	`MonoidHom.range` `Units` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `idemSemiring` `Units.instGroup` `CommRing.Pic` `CommGroup.toGroup` `instCommGroupPic` `unitsToPic` `CommRing.relPic`	—	`Subgroup.ext` `instSmallUnitsSkeletonSemimoduleCat` `Module.Invertible.instTensorProduct_2` `instInvertibleCarrierOutSemimoduleCatValSkeleton` `IsScalarTower.right` `Module.Invertible.inst` `RingHomInvPair.ids` `CommRing.Pic.mk_eq_one_iff` `IsScalarTower.to_smulCommClass` `RingHomCompTriple.ids` `Algebra.to_smulCommClass` `smulCommClass_self` `TensorProduct.smulCommClass_left` `IsScalarTower.to_smulCommClass'` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass` `Subgroup.instSubgroupClass` `isUnit_of_mul_isUnit_left` `instIsDedekindFiniteMonoid` `Module.Flat.of_projective` `Module.Invertible.instProjective` `IsScalarTower.left` `CommRing.Pic.mk_tensor` `CommRing.Pic.mk_eq_self` `mul_inv_cancel` `eq_span_singleton_of_surjective` `LinearEquiv.surjective` `mem_mul_span_singleton` `mem_top` `Module.Flat.top_mul_submoduleAlgebra` `IsUnit.map` `MonoidHom.instMonoidHomClass` `IsUnit.of_mul_eq_one_right` `instInvertibleSubtypeMemVal` `CommRing.Pic.mk_eq_iff`
`unitsQuotEquivRelPic_apply_coe` 📖	mathematical	—	`CommRing.Pic` `Subgroup` `CommGroup.toGroup` `instCommGroupPic` `SetLike.instMembership` `Subgroup.instSetLike` `CommRing.relPic` `DFunLike.coe` `MulEquiv` `HasQuotient.Quotient` `Units` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `idemSemiring` `Units.instGroup` `QuotientGroup.instHasQuotientSubgroup` `MonoidHom.range` `Units.map` `MonoidWithZeroHom.toMonoidHom` `NonAssocSemiring.toMulZeroOneClass` `spanSingleton` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `QuotientGroup.Quotient.group` `Subgroup.normal_of_comm` `Units.instCommGroupUnits` `CommSemiring.toCommMonoid` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `Subgroup.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `unitsQuotEquivRelPic` `Set` `Set.instMembership` `Set.range` `MonoidHom` `MonoidHom.instFunLike` `unitsToPic` `MonoidHom.ker` `QuotientGroup.quotientKerEquivRange` `QuotientGroup.congr` `MulEquiv.refl`	—	`instSmallUnitsSkeletonSemimoduleCat` `Subgroup.normal_of_comm`
`unitsQuotEquivRelPic_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `CommRing.Pic` `Subgroup` `CommGroup.toGroup` `instCommGroupPic` `SetLike.instMembership` `Subgroup.instSetLike` `CommRing.relPic` `HasQuotient.Quotient` `Units` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `idemSemiring` `Units.instGroup` `QuotientGroup.instHasQuotientSubgroup` `MonoidHom.range` `Units.map` `MonoidWithZeroHom.toMonoidHom` `NonAssocSemiring.toMulZeroOneClass` `spanSingleton` `Subgroup.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `QuotientGroup.Quotient.group` `Subgroup.normal_of_comm` `Units.instCommGroupUnits` `CommSemiring.toCommMonoid` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `unitsQuotEquivRelPic` `MonoidHom.ker` `unitsToPic` `QuotientGroup.congr` `MulEquiv.refl` `Subgroup.map` `MonoidHomClass.toMonoidHom` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `Subgroup.map_symm_eq_iff_map_eq` `QuotientGroup.quotientKerEquivRange` `MulEquiv.subgroupCongr` `range_unitsToPic`	—	`Subgroup.normal_of_comm`
`unitsToPic_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Units` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `idemSemiring` `CommRing.Pic` `MulOneClass.toMulOne` `Units.instMulOneClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroupPic` `MonoidHom.instFunLike` `unitsToPic` `SetLike.instMembership` `setLike` `Units.val` `addCommMonoid` `module` `instInvertibleSubtypeMemVal`	—	`instSmallUnitsSkeletonSemimoduleCat`

(root)

Definitions

Name	Category	Theorems
`instCommGroupPic` 📖	CompOp	28 math math: `CommRing.Pic.mk_dual`, `CommRing.Pic.mapAlgebra_self`, `CommRing.Pic.mul_eq_tensor`, `Submodule.ker_unitsToPic`, `CommRing.Pic.mk_tensor`, `CommRing.Pic.mapRingHom_id_apply`, `CommRing.relPic_eq_top`, `CommRing.Pic.mk_eq_one`, `CommRing.Pic.inv_eq_dual`, `CommRing.Pic.mapAlgebra_apply`, `CommRing.Pic.mk_eq_one_iff`, `CommRing.Pic.instFreeAsModuleOfNat`, `CommRing.Pic.mapAlgebra_comp_mapAlgebra`, `CommRing.Pic.mapRingHom_id`, `CommRing.Pic.mapAlgebra_self_apply`, `Submodule.unitsToPic_apply`, `Submodule.range_unitsToPic`, `Submodule.unitsQuotEquivRelPic_symm_apply`, `CommRing.Pic.mapRingHom_mapRingHom`, `ClassGroup.equivPic_symm_apply`, `CommRing.Pic.mk_eq_one_iff_free`, `CommRing.Pic.mapRingHom_comp_mapRingHom`, `Submodule.mulExact_unitsMap_spanSingleton_unitsToPic`, `CommRing.Pic.mk_self`, `ClassGroup.equivPic_apply`, `Submodule.mulExact_unitsToPic_mapAlgebra`, `CommRing.Pic.mapAlgebra_mapAlgebra`, `Submodule.unitsQuotEquivRelPic_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instInvertibleCarrierOutModuleCatValSkeleton` 📖	mathematical	—	`Module.Invertible` `ModuleCat.carrier` `CommRing.toRing` `Quotient.out` `ModuleCat` `CategoryTheory.isIsomorphicSetoid` `ModuleCat.moduleCategory` `Units.val` `CategoryTheory.Skeleton` `CategoryTheory.Skeleton.instMonoid` `ModuleCat.monoidalCategory` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule`	—	`Module.Invertible.right` `Quotient.eq` `Units.inv_mul`
`instInvertibleCarrierOutSemimoduleCatValSkeleton` 📖	mathematical	—	`Module.Invertible` `SemimoduleCat.carrier` `CommSemiring.toSemiring` `Quotient.out` `SemimoduleCat` `CategoryTheory.isIsomorphicSetoid` `SemimoduleCat.moduleCategory` `Units.val` `CategoryTheory.Skeleton` `CategoryTheory.Skeleton.instMonoid` `SemimoduleCat.monoidalCategory` `SemimoduleCat.isAddCommMonoid` `SemimoduleCat.isModule`	—	`Module.Invertible.right` `Quotient.eq` `Units.inv_mul`
`instInvertibleReprₛ` 📖	mathematical	—	`Module.Invertible` `Module.Finite.reprₛ` `CommSemiring.toSemiring` `Module.Invertible.instFinite` `ModuleCon.instAddCommMonoidQuotient` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Pi.addCommMonoid` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `DFunLike.coe` `LinearMap.instFunLike` `Module.Finite.exists_fin'` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Module.Finite.kerReprₛ` `ModuleCon.instModuleQuotient`	—	`Module.Invertible.congr` `Module.Invertible.instFinite` `Module.Finite.exists_fin'` `RingHomInvPair.ids`
`instSmallUnitsSkeletonModuleCat` 📖	mathematical	—	`Small` `Units` `CategoryTheory.Skeleton` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `CategoryTheory.Skeleton.instMonoid` `ModuleCat.monoidalCategory`	—	`small_map` `instSmallUnitsSkeletonSemimoduleCat`
`instSmallUnitsSkeletonSemimoduleCat` 📖	mathematical	—	`Small` `Units` `CategoryTheory.Skeleton` `SemimoduleCat` `CommSemiring.toSemiring` `SemimoduleCat.moduleCategory` `CategoryTheory.Skeleton.instMonoid` `SemimoduleCat.monoidalCategory`	—	`RingHomInvPair.ids` `Module.Finite.exists_fin'` `Module.Invertible.instFinite` `instInvertibleCarrierOutSemimoduleCatValSkeleton` `small_of_injective` `small_sigma` `UnivLE.small` `univLE_of_max` `UnivLE.self` `Units.ext` `Quotient.out_equiv_out` `RingHomCompTriple.ids`
`instSubsingletonPicOfIsDomainOfNonemptyNormalizedGCDMonoid` 📖	mathematical	—	`CommRing.Pic` `CommRing.toCommSemiring`	—	`Equiv.subsingleton` `NormalizedGCDMonoid.subsingleton_classGroup`

---

← Back to Index