|
117 | 117 | ["defsWithUnderscore", "CovariantDerivative.finite_affine_combination"], |
118 | 118 | ["defsWithUnderscore", |
119 | 119 | "CovariantDerivative.of_isCovariantDerivativeOn_of_open_cover"], |
120 | | - ["defsWithUnderscore", "DirectSum.congr_addEquiv"], |
121 | | - ["defsWithUnderscore", "DirectSum.congr_linearEquiv"], |
122 | 120 | ["defsWithUnderscore", "DirichletCharacter.primitive_mul"], |
123 | 121 | ["defsWithUnderscore", "DividedPowers.ideal_from_ringHom"], |
124 | 122 | ["defsWithUnderscore", "DividedPowers.subDPIdeal_inf_of_quot"], |
|
159 | 157 | ["defsWithUnderscore", "Int.le_induction"], |
160 | 158 | ["defsWithUnderscore", "Int.le_induction_down"], |
161 | 159 | ["defsWithUnderscore", "IntermediateField.restrict_algEquiv"], |
162 | | - ["defsWithUnderscore", "IsLocalDiffeomorph.diffeomorph_of_bijective"], |
163 | | - ["defsWithUnderscore", "IsLocalFrameOn.fintype_of_finiteDimensional"], |
164 | | - ["defsWithUnderscore", "IsLocalHomeomorph.toHomeomorph_of_bijective"], |
165 | 160 | ["defsWithUnderscore", "IsLocalization.invertible_mk'_one"], |
166 | 161 | ["defsWithUnderscore", "IsUltrametricDist.ball_openAddSubgroup"], |
167 | 162 | ["defsWithUnderscore", "IsUltrametricDist.ball_openSubgroup"], |
|
184 | 179 | ["defsWithUnderscore", "Matrix.equiv_GL_linearindependent"], |
185 | 180 | ["defsWithUnderscore", "Matroid.aesop_mat"], |
186 | 181 | ["defsWithUnderscore", "MeasureTheory.tacticVolume_tac"], |
187 | | - ["defsWithUnderscore", "ModelWithCorners.of_convex_range"], |
188 | | - ["defsWithUnderscore", "ModelWithCorners.of_target_univ"], |
189 | 182 | ["defsWithUnderscore", "ModularForm.eisensteinSeries_MF"], |
190 | 183 | ["defsWithUnderscore", "ModularForm.eta_q"], |
191 | 184 | ["defsWithUnderscore", "ModuleCat.forget₂AddCommGroup_preservesLimitsAux"], |
|
219 | 212 | ["defsWithUnderscore", "Ordinal.pred_succ_gi"], |
220 | 213 | ["defsWithUnderscore", "PadicInt.addChar_of_value_at_one"], |
221 | 214 | ["defsWithUnderscore", "PadicInt.continuousAddCharEquiv_of_norm_mul"], |
222 | | - ["defsWithUnderscore", "PadicInt.dividedPowers_of_injective"], |
223 | 215 | ["defsWithUnderscore", "Polynomial.divX_hom"], |
224 | 216 | ["defsWithUnderscore", "Polynomial.hilbertPoly_linearMap"], |
225 | 217 | ["defsWithUnderscore", "Polynomial.smul_pow"], |
|
310 | 302 | ["defsWithUnderscore", "lTensor.linearEquiv_of_rightInverse"], |
311 | 303 | ["defsWithUnderscore", "rTensor.inverse_of_rightInverse"], |
312 | 304 | ["defsWithUnderscore", "rTensor.linearEquiv_of_rightInverse"], |
313 | | - ["defsWithUnderscore", "AbsoluteValue.Completion.extensionEmbedding_of_comp"], |
314 | 305 | ["defsWithUnderscore", "AddChar.FiniteField.primitiveChar_to_Complex"], |
315 | 306 | ["defsWithUnderscore", "AddCommGrpCat.Colimits.isColimit_of_bijective_desc"], |
316 | 307 | ["defsWithUnderscore", "AlgEquiv.ofLinearEquiv_symm.aux"], |
|
431 | 422 | ["defsWithUnderscore", "Submodule.quotientPi_aux.invFun"], |
432 | 423 | ["defsWithUnderscore", "Submodule.quotientPi_aux.toFun"], |
433 | 424 | ["defsWithUnderscore", "SzemerediRegularity.Positivity.tacticSz_positivity"], |
434 | | - ["defsWithUnderscore", "Tactic.Interactive.tacticUnit_interval"], |
435 | 425 | ["defsWithUnderscore", "Tactic.ReduceModChar.reduce_mod_char"], |
436 | 426 | ["defsWithUnderscore", "Tactic.ReduceModChar.reduce_mod_char!"], |
437 | 427 | ["defsWithUnderscore", "TopCat.Presheaf.algebra_section_stalk"], |
|
530 | 520 | ["defsWithUnderscore", "Profinite.NobelingProof.GoodProducts.sum_to"], |
531 | 521 | ["defsWithUnderscore", "Stream'.WSeq.destruct_append.aux"], |
532 | 522 | ["defsWithUnderscore", "Stream'.WSeq.destruct_join.aux"], |
533 | | - ["defsWithUnderscore", "Mathlib.Meta.NormNum.NotPowerCertificate.pf_left"], |
534 | | - ["defsWithUnderscore", "Mathlib.Meta.NormNum.NotPowerCertificate.pf_right"], |
535 | 523 | ["defsWithUnderscore", |
536 | 524 | "CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.P"], |
537 | 525 | ["defsWithUnderscore", |
|
551 | 539 | ["defsWithUnderscore", "Mathlib.Meta.Finset.ProveEmptyOrConsResult.eq_trans"], |
552 | 540 | ["defsWithUnderscore", "Mathlib.Meta.List.ProveNilOrConsResult.eq_trans"], |
553 | 541 | ["defsWithUnderscore", "Mathlib.Meta.Multiset.ProveZeroOrConsResult.eq_trans"], |
| 542 | + ["defsWithUnderscore", "Mathlib.Meta.NormNum.NotPowerCertificate.pf_left"], |
| 543 | + ["defsWithUnderscore", "Mathlib.Meta.NormNum.NotPowerCertificate.pf_right"], |
554 | 544 | ["defsWithUnderscore", "Mathlib.Meta.NormNum.Result.eq_trans"], |
555 | 545 | ["defsWithUnderscore", |
556 | 546 | "CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.lift"], |
|
602 | 592 | ["docBlame", "IntermediateField.delabAdjoinNotation"], |
603 | 593 | ["docBlame", "IsAdjoinRoot.map"], |
604 | 594 | ["docBlame", "JordanHolderLattice.IsMaximal"], |
605 | | - ["docBlame", "JordanHolderLattice.Iso"], |
606 | 595 | ["docBlame", "Lean.ExportM"], |
607 | 596 | ["docBlame", "MaximalSpectrum.asIdeal"], |
608 | 597 | ["docBlame", "ModularForm.«term_∣[_]_»"], |
|
0 commit comments