OAI/GroupTheory/SimpleAmenable/RandomFields/FormalLawCovariance.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SimpleAmenable.InitialCoverSystem.smallPrimitiveEval_translate_localline 21 - theorem
OAI.SimpleAmenable.InitialCoverSystem.smallPrimitive_formal_translateline 39 - theorem
OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.translated_slope_coordinate_formal_lawline 65