Basic

📁 Source: FLT/Deformations/Algebra/InverseLimit/Basic.lean

Statistics

Metric	Count
Definitions `InverseSystemHom`, `instAdd`, `instAddActionOfAddActionHomClass`, `instAddCommGroupOfAddMonoidHomClass`, `instAddCommGroupWithOneOfAddMonoidHomClassOfOneHomClass`, `instAddCommMagmaOfAddHomClass`, `instAddCommMonoidOfAddMonoidHomClass`, `instAddCommMonoidWithOneOfAddMonoidHomClassOfOneHomClass`, `instAddCommSemigroupOfAddHomClass`, `instAddGroup`, `instAddGroupWithOne`, `instAddMonoid`, `instAddMonoidWithOne`, `instAddSemigroupOfAddHomClass`, `instAddZeroClassOfAddMonoidHomClass`, `instCoeOutForall`, `instCommGroupOfMonoidHomClass`, `instCommMagmaOfMulHomClass`, `instCommMonoidOfMonoidHomClass`, `instCommMonoidWithZeroOfMonoidWithZeroHomClass`, `instCommMonoidWithZeroOfMonoidWithZeroHomClass_1`, `instCommRingOfRingHomClass`, `instCommSemigroupOfMulHomClass`, `instCommSemiringOfRingHomClass`, `instDistribMulAction`, `instDistribSMulOfMulActionHomClass`, `instDivInvMonoid`, `instGroup`, `instModule`, `instMonoid`, `instMonoidWithZeroOfMonoidWithZeroHomClass`, `instMul`, `instMulActionOfMulActionHomClass`, `instMulDistribMulActionOfMulActionHomClass`, `instMulOneClassOfMonoidHomClass`, `instMulZeroClassOfMulHomClassOfZeroHomClass`, `instMulZeroOneClass`, `instNonAssocSemiringOfRingHomClass`, `instNonUnitalCommSemiringOfNonUnitalRingHomClass`, `instNonUnitalNonAssocCommSemiringOfNonUnitalRingHomClass`, `instNonUnitalNonAssocSemiringOfNonUnitalRingHomClass`, `instNonUnitalSemiringOfNonUnitalRingHomClass`, `instOne`, `instRingOfRingHomClass`, `instSMul`, `instSMulWithZeroOfMulActionHomClass`, `instSMulZeroClassOfMulActionHomClass`, `instSemigroupOfMulHomClass`, `instSemigroupWithZeroOfMulHomClassOfZeroHomClass`, `instSemiringOfRingHomClass`, `instVAdd`, `instZero`, `lift`, `liftLinearMap`, `liftMonoidHom`, `liftRingHom`, `toComponent`, `toComponentLinearMap`, `toComponentMonoidHom`, `toComponentRingHom`	60
Theorems `InverseLimit_def`, `add_def`, `div_def`, `div₀_def`, `ext_lemma`, `ext_lemma_iff`, `instNontrivial`, `intCast_def`, `inv_def`, `inv₀_def`, `lift_def`, `mul_def`, `natCast_def`, `neg_def`, `npow_def`, `nsmul_def`, `one_def`, `prop`, `smul_def`, `sub_def`, `toComponent_def`, `vadd_def`, `zero_def`, `zpow_def`, `zpow₀_def`, `zsmul_def`	26
Total	86

InverseLimit

Definitions

Name	Category	Theorems
`InverseSystemHom` 📖	MathDef	—
`instAdd` 📖	CompOp	1 math math: `add_def`
`instAddActionOfAddActionHomClass` 📖	CompOp	—
`instAddCommGroupOfAddMonoidHomClass` 📖	CompOp	1 math math: `instIsTopologicalModule`
`instAddCommGroupWithOneOfAddMonoidHomClassOfOneHomClass` 📖	CompOp	—
`instAddCommMagmaOfAddHomClass` 📖	CompOp	—
`instAddCommMonoidOfAddMonoidHomClass` 📖	CompOp	—
`instAddCommMonoidWithOneOfAddMonoidHomClassOfOneHomClass` 📖	CompOp	—
`instAddCommSemigroupOfAddHomClass` 📖	CompOp	—
`instAddGroup` 📖	CompOp	3 math math: `zsmul_def`, `sub_def`, `neg_def`
`instAddGroupWithOne` 📖	CompOp	1 math math: `intCast_def`
`instAddMonoid` 📖	CompOp	1 math math: `nsmul_def`
`instAddMonoidWithOne` 📖	CompOp	1 math math: `natCast_def`
`instAddSemigroupOfAddHomClass` 📖	CompOp	—
`instAddZeroClassOfAddMonoidHomClass` 📖	CompOp	—
`instCoeOutForall` 📖	CompOp	—
`instCommGroupOfMonoidHomClass` 📖	CompOp	—
`instCommMagmaOfMulHomClass` 📖	CompOp	—
`instCommMonoidOfMonoidHomClass` 📖	CompOp	—
`instCommMonoidWithZeroOfMonoidWithZeroHomClass` 📖	CompOp	—
`instCommMonoidWithZeroOfMonoidWithZeroHomClass_1` 📖	CompOp	—
`instCommRingOfRingHomClass` 📖	CompOp	—
`instCommSemigroupOfMulHomClass` 📖	CompOp	—
`instCommSemiringOfRingHomClass` 📖	CompOp	—
`instDistribMulAction` 📖	CompOp	—
`instDistribSMulOfMulActionHomClass` 📖	CompOp	—
`instDivInvMonoid` 📖	CompOp	3 math math: `div₀_def`, `inv₀_def`, `zpow₀_def`
`instGroup` 📖	CompOp	4 math math: `instIsTopologicalGroup`, `inv_def`, `zpow_def`, `div_def`
`instModule` 📖	CompOp	1 math math: `instIsTopologicalModule`
`instMonoid` 📖	CompOp	1 math math: `npow_def`
`instMonoidWithZeroOfMonoidWithZeroHomClass` 📖	CompOp	—
`instMul` 📖	CompOp	1 math math: `mul_def`
`instMulActionOfMulActionHomClass` 📖	CompOp	—
`instMulDistribMulActionOfMulActionHomClass` 📖	CompOp	—
`instMulOneClassOfMonoidHomClass` 📖	CompOp	—
`instMulZeroClassOfMulHomClassOfZeroHomClass` 📖	CompOp	—
`instMulZeroOneClass` 📖	CompOp	—
`instNonAssocSemiringOfRingHomClass` 📖	CompOp	—
`instNonUnitalCommSemiringOfNonUnitalRingHomClass` 📖	CompOp	—
`instNonUnitalNonAssocCommSemiringOfNonUnitalRingHomClass` 📖	CompOp	—
`instNonUnitalNonAssocSemiringOfNonUnitalRingHomClass` 📖	CompOp	—
`instNonUnitalSemiringOfNonUnitalRingHomClass` 📖	CompOp	—
`instOne` 📖	CompOp	1 math math: `one_def`
`instRingOfRingHomClass` 📖	CompOp	1 math math: `instIsTopologicalRing`
`instSMul` 📖	CompOp	1 math math: `smul_def`
`instSMulWithZeroOfMulActionHomClass` 📖	CompOp	—
`instSMulZeroClassOfMulActionHomClass` 📖	CompOp	—
`instSemigroupOfMulHomClass` 📖	CompOp	—
`instSemigroupWithZeroOfMulHomClassOfZeroHomClass` 📖	CompOp	—
`instSemiringOfRingHomClass` 📖	CompOp	—
`instVAdd` 📖	CompOp	1 math math: `vadd_def`
`instZero` 📖	CompOp	1 math math: `zero_def`
`lift` 📖	CompOp	2 math math: `lift_continuous`, `lift_def`
`liftLinearMap` 📖	CompOp	—
`liftMonoidHom` 📖	CompOp	—
`liftRingHom` 📖	CompOp	—
`toComponent` 📖	CompOp	2 math math: `toComponent_def`, `toComponent_continuous`
`toComponentLinearMap` 📖	CompOp	—
`toComponentMonoidHom` 📖	CompOp	—
`toComponentRingHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`InverseLimit_def` 📖	mathematical	—	`InverseLimit`	—	—
`add_def` 📖	mathematical	—	`InverseLimit` `instAdd`	—	—
`div_def` 📖	mathematical	—	`InverseLimit` `instGroup`	—	—
`div₀_def` 📖	mathematical	—	`InverseLimit` `instDivInvMonoid`	—	—
`ext_lemma` 📖	—	—	—	—	—
`ext_lemma_iff` 📖	—	—	—	—	`ext_lemma`
`instNontrivial` 📖	mathematical	—	`InverseLimit`	—	—
`intCast_def` 📖	mathematical	—	`InverseLimit` `instAddGroupWithOne`	—	—
`inv_def` 📖	mathematical	—	`InverseLimit` `instGroup`	—	—
`inv₀_def` 📖	mathematical	—	`InverseLimit` `instDivInvMonoid`	—	—
`lift_def` 📖	mathematical	`InverseSystemHom`	`lift`	—	—
`mul_def` 📖	mathematical	—	`InverseLimit` `instMul`	—	—
`natCast_def` 📖	mathematical	—	`InverseLimit` `instAddMonoidWithOne`	—	—
`neg_def` 📖	mathematical	—	`InverseLimit` `instAddGroup`	—	—
`npow_def` 📖	mathematical	—	`InverseLimit` `instMonoid`	—	—
`nsmul_def` 📖	mathematical	—	`InverseLimit` `instAddMonoid`	—	—
`one_def` 📖	mathematical	—	`InverseLimit` `instOne`	—	—
`prop` 📖	—	—	—	—	—
`smul_def` 📖	mathematical	—	`InverseLimit` `instSMul`	—	—
`sub_def` 📖	mathematical	—	`InverseLimit` `instAddGroup`	—	—
`toComponent_def` 📖	mathematical	—	`toComponent`	—	—
`vadd_def` 📖	mathematical	—	`InverseLimit` `instVAdd`	—	—
`zero_def` 📖	mathematical	—	`InverseLimit` `instZero`	—	—
`zpow_def` 📖	mathematical	—	`InverseLimit` `instGroup`	—	—
`zpow₀_def` 📖	mathematical	—	`InverseLimit` `instDivInvMonoid`	—	—
`zsmul_def` 📖	mathematical	—	`InverseLimit` `instAddGroup`	—	—

---

← Back to Index