Structures

📁 Source: Mathlib/Geometry/Manifold/Algebra/Structures.lean

Statistics

Metric	Count
Definitions ContMDiffRing	1
Theorems contMDiff_mul, toContMDiffAdd, toContMDiffMul, toLieAddGroup, instFieldContMDiffRing, topologicalSemiring_of_contMDiffRing	6
Total	7

ContMDiffRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiff_mul 📖	mathematical	—	ContMDiff Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod instTopologicalSpaceProd prodChartedSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—
toContMDiffAdd 📖	mathematical	—	ContMDiffAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—
toContMDiffMul 📖	mathematical	—	ContMDiffMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	ContMDiffAdd.toIsManifold toContMDiffAdd contMDiff_mul
toLieAddGroup 📖	mathematical	—	LieAddGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	StructureGroupoid.compatible IsManifold.toHasGroupoid ContMDiffMul.toIsManifold toContMDiffMul contMDiff_add toContMDiffAdd neg_one_mul contMDiff_mul_left

(root)

Definitions

Name	Category	Theorems
ContMDiffRing 📖	CompData	1 math math: instFieldContMDiffRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFieldContMDiffRing 📖	mathematical	—	ContMDiffRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace modelWithCornersSelf DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf	—	instNormedSpaceLieAddGroup LieAddGroup.toContMDiffAdd contMDiff_iff IsManifold.prod ContMDiffAdd.toIsManifold instContMDiffAddSelf continuous_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing PartialEquiv.trans_refl PartialEquiv.refl_prod_refl PartialEquiv.refl_trans Set.inter_univ contDiffOn_univ contDiff_mul
topologicalSemiring_of_contMDiffRing 📖	mathematical	—	IsTopologicalSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	continuousMul_of_contMDiffMul ContMDiffRing.toContMDiffMul continuousAdd_of_contMDiffAdd ContMDiffRing.toContMDiffAdd

---

← Back to Index