UnitsOfNormedAlgebra

📁 Source: Mathlib/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.lean

Statistics

Metric	Count
Definitions instChartedSpace	1
Theorems chartAt_apply, chartAt_source, contMDiff_val, instIsManifoldModelWithCornersSelf, instLieGroupModelWithCornersSelf	5
Total	6

Units

Definitions

Name	Category	Theorems
instChartedSpace 📖	CompOp	5 math math: instIsManifoldModelWithCornersSelf, instLieGroupModelWithCornersSelf, contMDiff_val, chartAt_source, chartAt_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
chartAt_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing instTopologicalSpaceUnits UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing chartAt instChartedSpace val	—	—
chartAt_source 📖	mathematical	—	PartialEquiv.source Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceUnits UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing chartAt instChartedSpace Set.univ	—	—
contMDiff_val 📖	mathematical	—	ContMDiff NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing instTopologicalSpaceUnits SeminormedRing.toPseudoMetricSpace instChartedSpace chartedSpaceSelf val	—	contMDiff_isOpenEmbedding isOpenEmbedding_val instHasSummableGeomSeriesOfCompleteSpace
instIsManifoldModelWithCornersSelf 📖	mathematical	—	IsManifold NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing instTopologicalSpaceUnits SeminormedRing.toPseudoMetricSpace instChartedSpace	—	Topology.IsOpenEmbedding.isManifold_singleton isOpenEmbedding_val instHasSummableGeomSeriesOfCompleteSpace
instLieGroupModelWithCornersSelf 📖	mathematical	—	LieGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing modelWithCornersSelf Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing instGroup instTopologicalSpaceUnits SeminormedRing.toPseudoMetricSpace instChartedSpace	—	instIsManifoldModelWithCornersSelf ContMDiff.of_comp_isOpenEmbedding isOpenEmbedding_val instHasSummableGeomSeriesOfCompleteSpace ContMDiff.prodMk_space ContMDiff.comp contMDiff_val contMDiff_fst contMDiff_snd contMDiff_iff_contDiff contDiff_mul Ring.inverse_invertible invOf_units ContMDiff.eq_1 ContMDiffAt.comp contMDiffAt_iff_contDiffAt contDiffAt_ringInverse

---

← Back to Index