forked from siddhartha-gadgil/LeanAide
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathOmitted20.lean
101 lines (101 loc) · 5.33 KB
/
Omitted20.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 Function.Injective.field.proof_25
#check CategoryTheory.Comonad.coalgebraPreadditive.proof_13
#check CategoryTheory.Limits.Bicone.toCoconeFunctor.proof_4
#check HomogeneousLocalization.NumDenSameDeg.instCommMonoidNumDenSameDeg.proof_6
#check ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux
#check DFinsupp.lsum.proof_3
#check Subspace.orderIsoFiniteCodimDim.proof_5
#check CategoryTheory.whiskeringRight.proof_5
#check SmoothMap.group.proof_8
#check GradedTensorProduct.lift.proof_6
#check CategoryTheory.Idempotents.functorExtension₂_obj_map_f
#check CategoryTheory.curry.proof_3
#check ValuationSubring.unitGroupMulEquiv.proof_7
#check CategoryTheory.TwoSquare.EquivalenceJ.functor.proof_5
#check CategoryTheory.bifunctorComp₁₂Obj.proof_4
#check ContinuousLinearMap.extend.proof_5
#check MeasureTheory.AEStronglyMeasurable.convolution_integrand
#check GradedRing.projZeroRingHom.proof_3
#check galLift.proof_4
#check CategoryTheory.Limits.walkingParallelPairOpEquiv.proof_5
#check CategoryTheory.Idempotents.instFullKaroubiFunctorCategoryInstCategoryKaroubiFunctorKaroubiInstCategoryKaroubiCategoryKaroubiFunctorCategoryEmbedding.proof_3
#check PresheafOfModules.Hom.instAddCommGroupHomPresheafOfModulesToQuiverToCategoryStructInstCategoryPresheafOfModules.proof_3
#check CategoryTheory.finitaryExtensiveTopCatAux.proof_14
#check CategoryTheory.Comonad.coalgebraPreadditive.proof_19
#check CategoryTheory.Monad.algebraPreadditive.proof_17
#check Action.instLinearActionInstCategoryActionInstPreadditiveActionInstCategoryAction.proof_9
#check ContMDiffOn.clm_postcomp
#check HasStrictFDerivAt.eq_implicitFunctionOfComplemented
#check CategoryTheory.Comma.coconeOfPreservesIsColimit.proof_3
#check CliffordAlgebra.lift.proof_5
#check Path.Homotopy.reparam.proof_5
#check CategoryTheory.GradedObject.mapTrifunctor.proof_4
#check lTensor.inverse_of_rightInverse.proof_7
#check CategoryTheory.FreeBicategory.lift.proof_5
#check TensorProduct.AlgebraTensorModule.rightComm.proof_25
#check LinearEquiv.symm_trans_apply
#check IsDedekindDomain.HeightOneSpectrum.instAlgebraSubtypeAdicCompletionMemValuationSubringInstFieldAdicCompletionInstMembershipInstSetLikeValuationSubringAdicCompletionIntegersToCommSemiringToSemiringToSemiringToRingToDivisionRingToSubsemiringToSubring.proof_5
#check CochainComplex.HomComplex.Cocycle.instModuleCocycleToSemiringToAddCommMonoidInstAddCommGroupCocycle.proof_4
#check ContinuousLinearEquiv.automorphismGroup.proof_4
#check CategoryTheory.ComposableArrows.isoMk₄
#check Finmap.keysLookupEquiv.proof_3
#check MeasureTheory.Lp.simpleFunc.module.proof_8
#check ChainComplex.augmentTruncate.proof_6
#check Function.Injective.kleeneAlgebra.proof_2
#check Module.Baer.ExtensionOf.inhabited.proof_5
#check ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one
#check ZNum.linearOrderedCommRing.proof_7
#check MeasureTheory.integrable_condexpL2_indicator
#check CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj.proof_5
#check CochainComplex.shiftFunctorAdd'.proof_3
#check FirstOrder.Language.DirectLimit.lift.proof_3
#check Profinite.NobelingProof.spanCone_isLimit.proof_5
#check Rep.ihom.proof_7
#check CategoryTheory.functorCategoryLinear.proof_7
#check HasCompactSupport.hasFDerivAt_convolution_right
#check Algebra.pushoutDesc.proof_4
#check CategoryTheory.FreeMonoidalCategory.project.proof_8
#check AddCircle.liftIco_eq_lift_Icc
#check CategoryTheory.discreteCategory.proof_13
#check CochainComplex.mappingCone.shiftIso.proof_5
#check CategoryTheory.GradedObject.mapTrifunctor.proof_3
#check CategoryTheory.symmetricOfHasFiniteCoproducts.proof_5
#check CategoryTheory.ComposableArrows.homMk
#check SmoothMap.compLeftMonoidHom.proof_1
#check NonUnitalAlgHom.equalizer.proof_4
#check CochainComplex.mk.proof_1
#check ContMDiffAt.coordChange
#check Bool.linearOrder.proof_6
#check ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear
#check HomologicalComplex.homologicalComplexToDGO.proof_3
#check CategoryTheory.CommSq.leftAdjointLiftStructEquiv.proof_5
#check CategoryTheory.preadditiveCoyoneda.proof_4
#check ContinuousLinearMap.compContinuousMultilinearMapL.proof_8
#check ConditionallyCompleteLattice.copy.proof_12
#check CategoryTheory.GradedObject.isColimitCofan₃MapBifunctor₁₂BifunctorMapObj.proof_8
#check LinearMap.exists_map_addHaar_eq_smul_addHaar'
#check CochainComplex.mappingCone.ext_from_iff
#check ContMDiffWithinAt.prod_mk
#check CategoryTheory.curry_obj_map_app
#check CategoryTheory.Functor.mapDifferentialObject.proof_4
#check CategoryTheory.functorCategoryLinear.proof_6
#check CategoryTheory.evaluationRightAdjoint_map_app
#check ConditionallyCompleteLattice.copy.proof_11
#check ZMod.commRing.proof_23
#check LieModule.exists_forall_mem_rootSpaceProductNegSelf_smul_add_eq_zero
#check PEquiv.instSemilatticeInfPEquiv.proof_4
#check LeftInvariantDerivation.left_invariant''
#check Real.commRing.proof_12
#check ZMod.commRing.proof_7
#check Submodule.Quotient.equiv.proof_9
#check Module.Baer.ExtensionOfMaxAdjoin.idealTo.proof_3
#check Zsqrtd.lift.proof_7
#check Perfection.lift.proof_9
#check LinearPMap.instSubtractionCommMonoid.proof_6
#check SSet.Augmented.standardSimplex.proof_5
#check CategoryTheory.Pseudofunctor.comp.proof_3
#check lTensor.inverse_comp_lTensor
#check AlgebraicGeometry.StructureSheaf.comap.proof_4
#check HomologicalComplex₂.flipFunctor.proof_3
#check ContinuousLinearEquiv.arrowCongrSL.proof_7