forked from siddhartha-gadgil/LeanAide
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathOmitted17.lean
101 lines (101 loc) · 5.19 KB
/
Omitted17.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
import Mathlib
#check Real.instDistribLatticeReal.proof_10
#check CategoryTheory.Over.ConstructProducts.conesEquivFunctor.proof_4
#check ModuleCat.normalEpi.proof_8
#check TensorAlgebra.lift.proof_4
#check ContinuousLinearEquiv.equivOfRightInverse_symm_apply
#check ContMDiff.coordChangeL
#check Function.Injective.divisionRing.proof_14
#check ValuationRing.linearOrder.proof_4
#check NonUnitalSubalgebra.instInvolutiveStar.proof_5
#check SubmodulesBasis.toModuleFilterBasis.proof_9
#check TopCommRingCat.instCategoryTopCommRingCat.proof_5
#check AlgebraCat.HasLimits.limitConeIsLimit.proof_7
#check Path.Homotopy.map.proof_4
#check Smooth.coordChange
#check CategoryTheory.GradedObject.ι_mapBifunctorComp₂₃MapObjIso_inv
#check ContMDiffOn.coordChangeL
#check MeasureTheory.lintegral_nnnorm_condexpL2_indicator_le
#check MDifferentiableOn.comp
#check ContinuousAffineMap.toConstProdContinuousLinearMap.proof_12
#check CategoryTheory.Comonad.coalgebraPreadditive.proof_16
#check LinearMap.BilinForm.tensorDistrib_tmul
#check CategoryTheory.ComposableArrows.homMk₄_app_three
#check AlgHom.extendScalars.proof_5
#check CategoryTheory.Limits.coneOfConeUncurryIsLimit.proof_3
#check Path.Homotopy.symm₂.proof_4
#check LinearPMap.instMulAction.proof_2
#check MultilinearMap.mkContinuousLinear.proof_6
#check CochainComplex.HomComplex.Cochain.rightUnshift_comp
#check CategoryTheory.Monad.algebraFunctorOfMonadHom.proof_5
#check CategoryTheory.ComposableArrows.homMk₅_app_three
#check homology'.map_desc_apply
#check Ordinal.monoid.proof_4
#check ContinuousMap.compStarAlgHom.proof_4
#check CategoryTheory.GradedObject.mapTrifunctorObj_map_app
#check CochainComplex.mappingCone.liftCochain_v_descCochain_v
#check CategoryTheory.CosimplicialObject.equivalenceRightToLeft.proof_4
#check apply_fdifferential
#check MvPowerSeries.map.proof_3
#check CategoryTheory.ShortComplex.limitCone.proof_4
#check MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left'
#check AlgebraicGeometry.scheme_restrict_basicOpen_of_localizationPreserves
#check CategoryTheory.Limits.coconeOfCoconeUncurryIsColimit.proof_3
#check CategoryTheory.Endofunctor.algebraPreadditive.proof_8
#check TrivSqZeroExt.liftEquiv.proof_7
#check IntermediateField.instPartialOrderLifts.proof_4
#check Submodule.equivSubtypeMap.proof_5
#check CategoryTheory.Monad.algebraPreadditive.proof_4
#check Submodule.localized'.proof_3
#check CategoryTheory.effectiveEpiFamilyStructOfIsColimit.proof_4
#check CategoryTheory.Comonad.coalgebraPreadditive.proof_17
#check UniversalEnvelopingAlgebra.lift.proof_3
#check CategoryTheory.effectiveEpiStructOfIsColimit.proof_3
#check CategoryTheory.Over.ConstructProducts.conesEquivCounitIso.proof_5
#check groupCohomology.dTwo.proof_2
#check CategoryTheory.Endofunctor.coalgebraPreadditive.proof_17
#check CategoryTheory.Limits.IsColimit.homIso'.proof_4
#check Poly.instAddCommGroupPoly.proof_10
#check Rep.ihom.proof_6
#check GromovHausdorff.instMetricSpaceGHSpace.proof_22
#check CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided.proof_12
#check CategoryTheory.SimplicialObject.equivalenceLeftToRight.proof_4
#check MultilinearMap.domDomCongrLinearEquiv'.proof_4
#check AffineMap.instAddTorsorAffineMapAddGroupIsAddTorsorToAddGroupAffineMapToAddGroupInstAddCommGroupAffineMapAddGroupIsAddTorsorToAddGroup.proof_6
#check Ordinal.partialOrder.proof_6
#check SmoothMap.restrictAddMonoidHom.proof_3
#check Function.Injective.kleeneAlgebra.proof_3
#check Ideal.quotientToQuotientRangePowQuotSucc_surjective
#check CategoryTheory.Subgroupoid.coe.proof_7
#check latToBddLatForgetAdjunction.proof_6
#check CategoryTheory.LaxMonoidalFunctor.mapMon.proof_5
#check ValuationRing.linearOrderedCommGroupWithZero.proof_6
#check TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse.proof_2
#check GromovHausdorff.instMetricSpaceGHSpace.proof_21
#check CategoryTheory.CechNerveTerminalFrom.wideCospan.limitCone.proof_4
#check AffineSubspace.equivMapOfInjective.proof_8
#check ContinuousMonoidHom.instCommGroupContinuousMonoidHomToMonoidToDivInvMonoidToGroup.proof_13
#check CategoryTheory.evaluationLeftAdjoint.proof_9
#check CategoryTheory.ShortComplex.isColimitOfIsColimitπ.proof_4
#check Function.Injective.orderedRing.proof_1
#check continuousMultilinearCurryRightEquiv.proof_17
#check ModuleCat.restrictCoextendScalarsAdj.proof_4
#check SmoothMonoidMorphism.mk.sizeOf_spec
#check CategoryTheory.evaluationAdjunctionLeft.proof_7
#check HomologicalComplex.singleMapHomologicalComplex.proof_7
#check LinearMap.lsum.proof_4
#check CategoryTheory.Monad.algebraPreadditive.proof_14
#check HomologicalComplex.asFunctor.proof_4
#check smoothSheafCommRing.forgetStalk_inv_comp_eval_assoc
#check LocalizedModule.instMonoidLocalizedModuleToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModule.proof_3
#check CategoryTheory.Quotient.preadditive.proof_12
#check Multiset.toFinsupp.proof_4
#check ZNum.linearOrderedCommRing.proof_18
#check CategoryTheory.transferNatTrans.proof_3
#check Finset.piAntidiagonal_insert
#check Trivialization.smoothWithinAt_iff
#check Bundle.ContinuousLinearMap.vectorPrebundle.proof_11
#check Finsupp.lsum.proof_4
#check IsAdjoinRootMonic.basis.proof_5
#check CategoryTheory.Functor.Initial.extendCone.proof_4
#check CategoryTheory.LiftAdjoint.constructLeftAdjointEquiv_symm_apply