forked from siddhartha-gadgil/LeanAide
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathOmitted26.lean
101 lines (101 loc) · 5.1 KB
/
Omitted26.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 CategoryTheory.Ran.equiv.proof_4
#check ContinuousMultilinearMap.currySumEquiv.proof_13
#check FiberBundleCore.trivChange.proof_7
#check LinearMap.toMatrix₂_compl₂
#check RingQuot.starRing.proof_2
#check CochainComplex.shiftFunctorZero'.proof_3
#check LinearEquiv.ofSubmodule'_symm_apply
#check CategoryTheory.bifunctorComp₁₂.proof_4
#check CategoryTheory.Pseudofunctor.comp.proof_5
#check CategoryTheory.Over.iteratedSliceEquiv.proof_6
#check CategoryTheory.ComposableArrows.homMk₅_app_one
#check VectorPrebundle.coordChange.proof_2
#check IsROrC.toStrictOrderedCommRing.proof_5
#check IsDedekindDomain.selmerGroup.proof_4
#check UniformEquiv.changeInv.proof_4
#check StarAlgHomClass.ext_topologicalClosure
#check Trivialization.coordChangeL_apply'
#check StarAlgEquiv.ofLeftInverse'_apply
#check LinearEquiv.arrowCongr.proof_8
#check ContinuousLinearMap.fderivWithin_of_bilinear
#check LinearPMap.adjointDomain.proof_5
#check SmoothMap.restrictMonoidHom.proof_2
#check SmoothOn.prod_map
#check CliffordAlgebra.even.ι.proof_6
#check Diffeomorph.coe_trans
#check CategoryTheory.Monad.algebraPreadditive.proof_18
#check CategoryTheory.ShortComplex.colimitCocone.proof_4
#check TensorProduct.tensorTensorTensorAssoc_symm_tmul
#check galRestrictHom.proof_6
#check EisensteinSeries.gammaSetEquiv.proof_3
#check Matrix.PosSemidef.toLinearMap₂'_zero_iff
#check MeasureTheory.condexpL1CLM_of_aestronglyMeasurable'
#check GradedTensorProduct.instMonoid.proof_3
#check CategoryTheory.ComposableArrows.isoMk₄_inv
#check ContinuousLinearEquiv.map_tsum
#check CategoryTheory.Over.ConstructProducts.conesEquivFunctor.proof_5
#check CategoryTheory.Endofunctor.algebraPreadditive.proof_19
#check smoothOn_continuousLinearMapCoordChange
#check CategoryTheory.Endofunctor.coalgebraPreadditive.proof_11
#check Submodule.completeLattice.proof_9
#check CategoryTheory.Arrow.cechConerve.proof_6
#check CategoryTheory.Limits.IsLimit.homIso'.proof_3
#check iteratedFDerivWithin_succ_eq_comp_left
#check AlgebraicGeometry.StructureSheaf.sectionsSubring.proof_5
#check AlgebraicGeometry.Scheme.OpenCover.finiteSubcover.proof_3
#check ModuleCat.binaryProductLimitCone.proof_3
#check CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj.proof_4
#check AlgebraicGeometry.PresheafedSpace.componentwiseDiagram.proof_3
#check Mod_.comap.proof_3
#check CategoryTheory.coyonedaPreservesLimits.proof_2
#check Complex.commRing.proof_8
#check ContinuousLinearEquiv.arrowCongrSL
#check Complex.integral_boundary_rect_of_differentiableOn_real
#check Matrix.toLinearMap₂_apply
#check RatFunc.instAlgebraRatFuncToSemiringToDivisionSemiringToSemifieldInstField.proof_6
#check TopCommRingCat.instCategoryTopCommRingCat.proof_4
#check CategoryTheory.GradedObject.mapBifunctorMap_map_app
#check HilbertBasis.coe_mk
#check CategoryTheory.Monad.algebraPreadditive.proof_8
#check GradedTensorProduct.comm.proof_7
#check PartialHomeomorph.MDifferentiable.ker_mfderiv_eq_bot
#check NonUnitalStarSubalgebra.unitizationStarAlgEquiv.proof_13
#check LieModule.coe_maxTrivLinearMapEquivLieModuleHom_symm
#check SymplecticGroup.instGroupSubtypeMatrixSumMemSubmonoidToMulOneClassToMulZeroOneClassNonAssocSemiringToNonAssocSemiringToSemiringToCommSemiringInstFintypeSumInstDecidableEqSumInstMembershipInstSetLikeSubmonoidSymplecticGroup.proof_19
#check Finsupp.basis.proof_2
#check LeftInvariantDerivation.instSubLeftInvariantDerivation.proof_3
#check ContinuousLinearMap.aestronglyMeasurable_comp₂
#check CliffordAlgebra.foldr'Aux.proof_8
#check CategoryTheory.Pi.sum.proof_3
#check ContinuousMultilinearMap.curryFinFinset_apply
#check VectorPrebundle.mk_smoothCoordChange
#check LieModule.shiftedWeightSpace.toEndomorphism_eq
#check CategoryTheory.yonedaPreservesLimits.proof_2
#check CategoryTheory.OplaxFunctor.comp.proof_1
#check Representation.linHom.proof_5
#check CategoryTheory.evaluation.proof_5
#check FirstOrder.Language.DirectLimit.lift.proof_4
#check ContMDiffWithinAt.clm_apply
#check hfdifferential.proof_4
#check TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso.proof_4
#check Finsupp.lsum.proof_7
#check RingSubgroupsBasis.toRingFilterBasis.proof_9
#check IsDedekindDomain.HeightOneSpectrum.instAlgebraSubtypeAdicCompletionMemValuationSubringInstFieldAdicCompletionInstMembershipInstSetLikeValuationSubringAdicCompletionIntegersToCommSemiringToSemiringToSemiringToRingToDivisionRingToSubsemiringToSubring.proof_4
#check HasStrictFDerivAt.to_implicitFunction
#check AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.MemCarrier.clear_denominator
#check Set.unitEquivUnitsInteger.proof_9
#check CategoryTheory.Functor.mapDifferentialObject_map_f
#check FiberBundleCore.localTriv.proof_6
#check SmoothMap.module'.proof_5
#check Diffeomorph.symm_trans'
#check Function.Injective.field.proof_3
#check ContinuousLinearEquiv.arrowCongrSL.proof_10
#check elementalStarAlgebra.starAlgHomClass_ext
#check MvPowerSeries.map.proof_4
#check SmoothMap.smul_comp
#check SmoothFiberwiseLinear.locality_aux₂
#check Submodule.fstEquiv.proof_5
#check SmoothBumpCovering.exists_immersion_euclidean
#check WeakDual.gelfandTransform_apply_apply
#check CategoryTheory.ShortComplex.FunctorEquivalence.counitIso.proof_4