Documentation Verification Report

Extension

📁 Source: Mathlib/Topology/Algebra/Group/Extension.lean

Statistics

Metric	Count
Definitions `Extension`, `Extension`, `Extension`, `Extension`, `IsSES`, `IsSES`	6
Theorems `exact`, `isClosedEmbedding`, `isOpenQuotientMap`, `ofClosedAddSubgroup`, `isClosedEmbedding`, `isOpenQuotientMap`, `mulExact`, `ofClosedSubgroup`	8
Total	14

Algebra

Definitions

Name	Category	Theorems
`Extension` 📖	CompData	—

FiniteField

Definitions

Name	Category	Theorems
`Extension` 📖	CompOp	12 math math: `Extension.frob_apply`, `card_algEquiv_extension`, `instIsSplittingFieldExtensionHSubPolynomialHPowNatXCard`, `instIsScalarTowerZModExtension`, `finrank_zmod_extension`, `instFiniteExtension_1`, `natCard_extension`, `nonempty_algHom_extension`, `Extension.exists_frob_pow_eq`, `natCard_algEquiv_extension`, `finrank_extension`, `Extension.frob_iterate_apply`

LieAlgebra

Definitions

Name	Category	Theorems
`Extension` 📖	CompData	—

NumberField.ComplexEmbedding

Definitions

Name	Category	Theorems
`Extension` 📖	CompOp	—

TopologicalAddGroup

Definitions

Name	Category	Theorems
`IsSES` 📖	CompData	1 math math: `IsSES.ofClosedAddSubgroup`

TopologicalAddGroup.IsSES

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exact` 📖	mathematical	`TopologicalAddGroup.IsSES`	`Function.Exact` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`isClosedEmbedding` 📖	mathematical	`TopologicalAddGroup.IsSES`	`Topology.IsClosedEmbedding` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike`	—	—
`isOpenQuotientMap` 📖	mathematical	`TopologicalAddGroup.IsSES`	`IsOpenQuotientMap` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike`	—	—
`ofClosedAddSubgroup` 📖	mathematical	—	`TopologicalAddGroup.IsSES` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `HasQuotient.Quotient` `QuotientAddGroup.instHasQuotientAddSubgroup` `AddSubgroup.toAddGroup` `QuotientAddGroup.Quotient.addGroup` `instTopologicalSpaceSubtype` `QuotientAddGroup.instTopologicalSpace` `AddSubgroup.subtype` `QuotientAddGroup.mk'`	—	`Topology.IsInducing.subtypeVal` `AddSubgroup.subtype_injective` `Subtype.range_coe_subtype` `AddAction.isOpenQuotientMap_quotientMk` `VAddCommClass.continuousConstVAdd` `AddSubgroup.vaddCommClass_left` `AddSemigroup.opposite_vaddCommClass` `instSeparatelyContinuousAddOfContinuousAdd` `IsTopologicalAddGroup.toContinuousAdd` `QuotientAddGroup.eq_zero_iff` `SetLike.mem_coe`

TopologicalGroup

Definitions

Name	Category	Theorems
`IsSES` 📖	CompData	1 math math: `IsSES.ofClosedSubgroup`

TopologicalGroup.IsSES

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosedEmbedding` 📖	mathematical	`TopologicalGroup.IsSES`	`Topology.IsClosedEmbedding` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	—	—
`isOpenQuotientMap` 📖	mathematical	`TopologicalGroup.IsSES`	`IsOpenQuotientMap` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	—	—
`mulExact` 📖	mathematical	`TopologicalGroup.IsSES`	`Function.MulExact` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`ofClosedSubgroup` 📖	mathematical	—	`TopologicalGroup.IsSES` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup` `Subgroup.toGroup` `QuotientGroup.Quotient.group` `instTopologicalSpaceSubtype` `QuotientGroup.instTopologicalSpace` `Subgroup.subtype` `QuotientGroup.mk'`	—	`Topology.IsInducing.subtypeVal` `Subgroup.subtype_injective` `Subtype.range_coe_subtype` `MulAction.isOpenQuotientMap_quotientMk` `SMulCommClass.continuousConstSMul` `Subgroup.smulCommClass_left` `Semigroup.opposite_smulCommClass` `instSeparatelyContinuousMulOfContinuousMul` `IsTopologicalGroup.toContinuousMul`

---

← Back to Index