Documentation Verification Report

Subgroup

📁 Source: Mathlib/Analysis/Normed/Group/Subgroup.lean

Statistics

Metric	Count
Definitions `normedAddCommGroup`, `normedAddGroup`, `seminormedAddCommGroup`, `seminormedAddGroup`, `normedAddCommGroup`, `normedAddGroup`, `seminormedAddCommGroup`, `seminormedAddGroup`, `normedCommGroup`, `normedGroup`, `seminormedCommGroup`, `seminormedGroup`, `normedCommGroup`, `normedGroup`, `seminormedCommGroup`, `seminormedGroup`	16
Theorems `coe_norm`, `norm_coe`, `coe_norm`, `coe_norm`, `norm_coe`, `coe_norm`	6
Total	22

AddSubgroup

Definitions

Name	Category	Theorems
`normedAddCommGroup` 📖	CompOp	42 math math: `MeasureTheory.L1.SimpleFunc.norm_Integral_le_one`, `MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left`, `MeasureTheory.L1.SimpleFunc.setToL1SCLM_const`, `AddCircle.isAddFundamentalDomain_of_ae_ball`, `MeasureTheory.L1.norm_setToL1_le_norm_setToL1SCLM`, `MeasureTheory.L1.SimpleFunc.norm_setToL1S_le`, `MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left'`, `MeasureTheory.L1.SimpleFunc.integral_eq_norm_posPart_sub`, `MeasureTheory.L1.setToL1_eq_setToL1SCLM`, `isAddFundamentalDomain_Ioc`, `MeasureTheory.L1.SimpleFunc.setToL1S_smul_real`, `MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left`, `MeasureTheory.L1.SimpleFunc.norm_eq_sum_mul`, `unitary.norm_argSelfAdjoint`, `ZSpan.isAddFundamentalDomain'`, `MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le'`, `MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left`, `MeasureTheory.Lp.simpleFunc.norm_toSimpleFunc`, `MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left'`, `MeasureTheory.L1.setToL1_apply_coeToLp`, `MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left'`, `MeasureTheory.lpMeasSubgroupToLpTrim_norm_map`, `MeasureTheory.L1.SimpleFunc.integral_smul`, `MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le`, `MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_measure`, `MeasureTheory.L1.SimpleFunc.norm_eq_integral`, `MeasureTheory.L1.SimpleFunc.norm_integral_le_norm`, `MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left'`, `MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left`, `Unitary.norm_argSelfAdjoint`, `MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left`, `unitary.norm_argSelfAdjoint_le_pi`, `MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono`, `Unitary.norm_argSelfAdjoint_le_pi`, `MeasureTheory.L1.setToL1'_eq_setToL1SCLM`, `MeasureTheory.L1.SimpleFunc.setToL1SCLM_nonneg`, `MeasureTheory.L1.setToL1'_apply_coeToLp`, `unitary.two_mul_one_sub_cos_norm_argSelfAdjoint`, `MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left'`, `MeasureTheory.Lp.simpleFunc.norm_toLp`, `MeasureTheory.L1.SimpleFunc.setToL1S_smul`, `Unitary.two_mul_one_sub_cos_norm_argSelfAdjoint`
`normedAddGroup` 📖	CompOp	—
`seminormedAddCommGroup` 📖	CompOp	26 math math: `MeasureTheory.L1.SimpleFunc.norm_Integral_le_one`, `NormedAddGroupHom.Equalizer.ι_normNoninc`, `NormedAddGroupHom.incl_range`, `MeasureTheory.L1.norm_setToL1_le_norm_setToL1SCLM`, `NormedAddGroupHom.Equalizer.map_normNoninc`, `realPart.norm_le`, `NormedAddGroupHom.Equalizer.liftEquiv_apply`, `imaginaryPart.norm_le`, `NormedAddGroupHom.range_comp_incl_top`, `NormedAddGroupHom.Equalizer.ι_comp_map`, `NormedAddGroupHom.Equalizer.lift_normNoninc`, `MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le'`, `NormedAddGroupHom.incl_apply`, `NormedAddGroupHom.Equalizer.ι_comp_lift`, `NormedAddGroupHom.Equalizer.lift_apply_coe`, `NormedAddGroupHom.ker_completion`, `MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le`, `NormedAddGroupHom.ker.incl_comp_lift`, `NormedAddGroupHom.Equalizer.map_comp_map`, `NormedAddGroupHom.Equalizer.comp_ι_eq`, `NormedAddGroupHom.ker_le_ker_completion`, `NormedAddGroupHom.Equalizer.map_id`, `NormedAddGroupHom.ker.lift_apply_coe`, `NormedAddGroupHom.Equalizer.norm_lift_le`, `NormedAddGroupHom.Equalizer.liftEquiv_symm_apply_coe`, `NormedAddGroupHom.norm_incl`
`seminormedAddGroup` 📖	CompOp	2 math math: `norm_coe`, `coe_norm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_norm` 📖	mathematical	—	`Norm.norm` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SetLike.instMembership` `instSetLike` `SeminormedAddGroup.toNorm` `seminormedAddGroup`	—	—
`norm_coe` 📖	mathematical	—	`Norm.norm` `SeminormedAddGroup.toNorm` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SetLike.instMembership` `instSetLike` `seminormedAddGroup`	—	—

AddSubgroupClass

Definitions

Name	Category	Theorems
`normedAddCommGroup` 📖	CompOp	—
`normedAddGroup` 📖	CompOp	—
`seminormedAddCommGroup` 📖	CompOp	—
`seminormedAddGroup` 📖	CompOp	1 math math: `coe_norm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_norm` 📖	mathematical	—	`Norm.norm` `SetLike.instMembership` `SeminormedAddGroup.toNorm` `seminormedAddGroup`	—	—

Subgroup

Definitions

Name	Category	Theorems
`normedCommGroup` 📖	CompOp	—
`normedGroup` 📖	CompOp	—
`seminormedCommGroup` 📖	CompOp	—
`seminormedGroup` 📖	CompOp	2 math math: `coe_norm`, `norm_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_norm` 📖	mathematical	—	`Norm.norm` `Subgroup` `SeminormedGroup.toGroup` `SetLike.instMembership` `instSetLike` `SeminormedGroup.toNorm` `seminormedGroup`	—	—
`norm_coe` 📖	mathematical	—	`Norm.norm` `SeminormedGroup.toNorm` `Subgroup` `SeminormedGroup.toGroup` `SetLike.instMembership` `instSetLike` `seminormedGroup`	—	—

SubgroupClass

Definitions

Name	Category	Theorems
`normedCommGroup` 📖	CompOp	—
`normedGroup` 📖	CompOp	—
`seminormedCommGroup` 📖	CompOp	—
`seminormedGroup` 📖	CompOp	1 math math: `coe_norm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_norm` 📖	mathematical	—	`Norm.norm` `SetLike.instMembership` `SeminormedGroup.toNorm` `seminormedGroup`	—	—

---

← Back to Index