Documentation Verification Report

Submodule

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

Statistics

Metric	Count
Definitions `normedAddCommGroup`, `seminormedAddCommGroup`	2
Theorems `coe_norm`, `norm_coe`	2
Total	4

Submodule

Definitions

Name	Category	Theorems
`normedAddCommGroup` 📖	CompOp	62 math math: `TensorProduct.mapInclIsometry_apply`, `ZLattice.summable_norm_zpow`, `Affine.Simplex.altitudeFoot_restrict`, `OrthonormalBasis.orthogonalProjection_eq_sum`, `IsHilbertSum.mkInternal`, `MeasureTheory.norm_condExpL2_le`, `instStrictConvexSpace`, `re_inner_starProjection_eq_normSq`, `OrthonormalBasis.orthogonalProjection_eq_sum_rankOne`, `Affine.Simplex.circumradius_restrict`, `ZLattice.tsum_norm_rpow_le`, `Affine.Simplex.ninePointCircle_restrict`, `OrthonormalBasis.orthogonalProjection_apply_eq_sum`, `EuclideanGeometry.Sphere.coe_secondInter`, `adjoint_subtypeL`, `ZLattice.tsumNormRPowBound_spec`, `contDiffOn_stereoToFun`, `HilbertBasis.hasSum_orthogonalProjection`, `stereoInvFun_apply`, `Affine.Simplex.altitude_restrict_eq_comap_subtype`, `norm_orthogonalProjection_apply_le`, `OrthonormalBasis.starProjection_eq_sum_rankOne`, `TensorProduct.inner_mapIncl_mapIncl`, `Affine.Simplex.ExcenterExists.touchpointWeights_restrict`, `EuclideanGeometry.orthogonalProjection_subtype`, `Affine.Simplex.ExcenterExists.excenter_restrict`, `norm_sq_eq_add_norm_sq_projection`, `ZLattice.summable_norm_rpow`, `Affine.Simplex.map_altitude_restrict`, `Affine.Simplex.exradius_restrict`, `Affine.Simplex.circumcenter_restrict`, `Affine.Simplex.height_restrict`, `ZLattice.summable_norm_pow_inv`, `Affine.Simplex.incenter_restrict`, `norm_orthogonalProjection_apply`, `Affine.Simplex.inradius_restrict`, `ZLattice.exists_forall_abs_repr_le_norm`, `DirectSum.IsInternal.subordinateOrthonormalBasis_def`, `Affine.Simplex.orthogonalProjectionSpan_restrict`, `Affine.Simplex.excenterWeights_restrict`, `Affine.Simplex.mongePoint_restrict`, `Affine.Simplex.eulerPoint_restrict`, `OrthonormalBasis.span_apply`, `Affine.Simplex.ExcenterExists.touchpoint_restrict`, `Affine.Simplex.excenterWeightsUnnorm_restrict`, `ContinuousLinearMap.IsPositive.orthogonalProjection_comp`, `adjoint_orthogonalProjection`, `ZLattice.le_norm_of_le_abs_repr`, `LinearIsometry.strictConvexSpace_range_iff`, `LinearIsometry.strictConvexSpace_range`, `angle_coe`, `ZLattice.normBound_spec`, `AffineSubspace.angle_coe`, `EuclideanGeometry.reflection_subtype`, `EuclideanGeometry.orthogonalProjection_apply`, `ZLattice.sum_piFinset_Icc_rpow_le`, `LinearMap.exists_map_addHaar_eq_smul_addHaar'`, `TensorProduct.toLinearMap_mapInclIsometry`, `ZLattice.exists_finsetSum_norm_rpow_le_tsum`, `isHilbertSumOrthogonal`, `ZLattice.abs_repr_le`, `Affine.Simplex.excenterExists_restrict`
`seminormedAddCommGroup` 📖	CompOp	69 math math: `orthogonalDecomposition_symm_apply`, `toLinearEquiv_orthogonalDecomposition_symm`, `LinearMap.IsSymmetric.diagonalization_apply_self_apply`, `AffineIsometryEquiv.ofTop_apply`, `toLinearEquiv_orthogonalDecomposition`, `Orthonormal.codRestrict`, `OrthonormalBasis.orthogonalProjection_eq_sum_rankOne`, `OrthogonalFamily.of_pairwise`, `LinearMap.IsSymmetric.orthogonalFamily_eigenspaces`, `subtypeₗᵢ_toContinuousLinearMap`, `coe_orthogonalDecomposition_symm`, `AffineSubspace.coe_subtypeₐᵢ`, `subtypeₗᵢ_toLinearMap`, `LinearEquiv.toSpanNonzeroSingleton_homothety`, `LinearIsometryEquiv.coe_ofEq_apply`, `LinearIsometry.equivRange_apply_coe`, `LinearIsometryEquiv.ofTop_toLinearEquiv`, `LinearIsometryEquiv.ofTop_symm_apply_coe`, `AffineIsometryEquiv.coe_ofEq_apply`, `AffineSubspace.isometryEquivMap.toAffineMap_eq`, `LinearMap.IsSymmetric.diagonalization_symm_apply`, `AffineIsometryEquiv.ofTop_symm_apply_coe`, `MeasureTheory.lpMeasToLpTrimLie_symm_indicator`, `LinearMap.IsSymmetric.restrict_invariant`, `AffineIsometryEquiv.ofEq_symm`, `LinearIsometry.extend_apply`, `coe_orthogonalDecomposition`, `norm_subtypeL`, `AffineSubspace.toContinuousAffineMap_subtypeₐᵢ`, `fst_orthogonalDecomposition_apply`, `orthogonalFamily_self`, `inner_orthogonalProjection_eq_of_mem_right`, `LinearMap.IsSymmetric.orthogonalFamily_eigenspaces'`, `LinearIsometryEquiv.toSpanUnitSingleton_apply`, `LinearMap.IsSymmetric.orthogonalFamily_eigenspace_inf_eigenspace`, `LinearIsometryEquiv.ofTop_apply`, `coe_inner`, `AffineSubspace.isometryEquivMap.coe_apply`, `sndL_comp_coe_orthogonalDecomposition`, `coe_subtypeₗᵢ`, `inner_orthogonalProjection_eq_of_mem_left`, `AffineSubspace.subtypeₐᵢ_linear`, `coord_norm'`, `LinearIsometryEquiv.submoduleMap_symm_apply_coe`, `AffineSubspace.subtypeₐᵢ_linearIsometry`, `AffineIsometryEquiv.ofEq_rfl`, `norm_coe`, `orthogonalFamily_iff_pairwise`, `fstL_comp_coe_orthogonalDecomposition`, `exists_extension_norm_eq`, `ContinuousLinearEquiv.coord_norm'`, `snd_orthogonalDecomposition_apply`, `AffineSubspace.isometryEquivMap.apply_symm_apply`, `coe_norm`, `orthogonalDecomposition_apply`, `LinearIsometryEquiv.ofEq_rfl`, `ContinuousLinearEquiv.coord_norm`, `norm_orthogonalProjection`, `AffineSubspace.subtypeₐᵢ_toAffineMap`, `Real.exists_extension_norm_eq`, `norm_subtypeL_le`, `MeasureTheory.lpMeasToLpTrimLie_symm_toLp`, `orthogonalProjection_norm_le`, `MeasureTheory.norm_condExpL2_le_one`, `LinearIsometry.submoduleMap_apply_coe`, `LinearMap.IsSymmetric.orthogonalFamily_iInf_eigenspaces`, `orthonormal_span`, `LinearIsometryEquiv.ofEq_symm`, `LinearIsometryEquiv.submoduleMap_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_norm` 📖	mathematical	—	`Norm.norm` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SetLike.instMembership` `setLike` `SeminormedAddCommGroup.toNorm` `seminormedAddCommGroup`	—	—
`norm_coe` 📖	mathematical	—	`Norm.norm` `SeminormedAddCommGroup.toNorm` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SetLike.instMembership` `setLike` `seminormedAddCommGroup`	—	—

---

← Back to Index