Fix merge conflict #2700
butterthebuddha
merged
1855 commits into
leanprover-community:primary-ideal
from
butterthebuddha:primary-ideal
chore(scripts): update nolints.txt (#2430)
7270af9c
refactor(tactic/norm_cast): simplified attributes and numeral support…
5fd4afc4
refactor(analysis/asymptotics): make is_o irreducible (#2416)
ec800611
feat(analysis/calculus): let simp compute derivatives (#2422)
846cbabb
chore(scripts): update nolints.txt (#2432)
a113d6e6
feat(computability): strong reducibility and degrees (#1203)
c3d943e2
chore(algebra/lie_algebra): add function coercion for morphisms (#2434)
d2db3e83
chore(scripts): update nolints.txt (#2435)
0d3e5465
feat(category_theory): creation of limits and reflection of isomorph…
f3471479
feat(category_theory/limits): strong epimorphisms and strong epi-mono…
0567b7fa
chore(scripts): update nolints.txt (#2436)
715be9f7
feat(analysis/analytic/composition): the composition of analytic func…
0bc15f82
feat(data/nat): Results about nat.choose (#2421)
855e70bf
chore(*): migrate `nat/int/rat.eq_cast` to bundled homs (#2427)
64f6903e
chore(scripts): update nolints.txt (#2440)
da292759
fix(github/workflows): ignore new bors branch (#2441)
24d464c6
feat(tactic/lint): lint for missing has_coe_to_fun instances (#2437)
6b095759
docs(install/*): put extra emphasis (#2439)
1ef989f8
refactor(data/nat/fib): simplify proof of fib_succ_succ (#2443)
a530a817
chore(data/mv_polynomial): adding a comment about a T50000 regression…
8b21231c
chore(algebra/group/type_tags): add `additive.to_mul` etc (#2363)
ffb99a33
feat(tactic/transport): transport structures across equivalences (#2251)
4e872238
fix(group_theory/submonoid): looping simp lemma (#2447)
16552e6a
fix(docs/extra/calc.md): remove extra space (#2448)
5107c2bd
fix(*): remove `@[nolint simp_nf]` (#2450)
8ec447d8
feat(category_theory/limits/over): over category has connected limits…
d76a882d
chore(*): switch to lean 3.9.0 (#2449)
99245b33
feat(data/nat/prime) factors of a prime number is the list [p] (#2452)
0ceac44d
chore(algebra/module): replace typeclass arguments with inferred argu…
11d89a2f
chore(category_theory/monoidal): some arguments that need to be made …
d344310e
chore(number_theory/sum_four_squares): slightly shorten proof (#2457)
6054f7c9
feat(continued_fractions) add stabilisation under termination lemmas …
9801c1c0
feat(category_theory/eq_to_iso): missing simp lemma (#2454)
aa55f8b5
fix(category_theory/limits): remove an unnecessary axiom in has_image…
e6aa533b
fix(category_theory/limits): make image.map_comp a simp lemma (#2456)
a8edb5e2
chore(tactic/simp_result): forgot to import in tactic.basic (#2462)
c0afa80e
fix(category_theory/limits): avoid a rewrite in a definition (#2458)
9b255781
fix(tactic/delta_instance): handle universe metavariables (#2463)
58088cc9
feat(category_theory/opposites): some opposite category properties (#…
44743821
chore(scripts): update nolints.txt (#2467)
59a767ee
chore(category_theory/opposites): typo fix (#2466)
036b0386
feat(data/monoid_algebra): the distrib_mul_action (#2417)
51e03aad
feat(category_theory/faithful): faithful.of_iso (#2453)
d1ba87a9
feat(data/nat,data/int): add some modular arithmetic lemmas (#2460)
8adfafd9
fix(algebra/category/*/colimits): cleaning up (#2469)
76267637
chore(docs/naming): update (#2468)
5d0a7240
chore(category_theory): delete two empty files (#2472)
7a13a11a
fix(category_theory/concrete): access the carrier type by the coercio…
3edb6a4a
fix(tactic/clear): don't use rb_map unnecessarily (#2325)
df84064e
feat(tactic/#simp): a user_command for #simp (#2446)
15d35b1a
feat(tactic/hint): if hint can solve the goal, say so (#2474)
533a5523
fix(tactic/where): remove hackery from `#where`, using Lean 3c APIs (…
ffa97d0f
chore(scripts): update nolints.txt (#2482)
585d77ae
feat(group_theory/bundled_subgroup): bundled subgroup (#2140)
5e2025f6
chore(cmd/where): remove unused argument (#2486)
142f0017
feat(data/monoid_algebra): algebra structure, lift of morphisms (#2366)
59653709
chore(data/polynomial): rename type vars (#2483)
e4abcedc
feat(data/option): add `option.mmap` and `option.maybe` (#2484)
62a613fa
chore(meta/expr): add a docstring (#2487)
f760ad5f
chore(tactic/auto_cases): add docstring and remove duplication (#2488)
d40662f5
chore(scripts): update nolints.txt (#2491)
8865b00a
chore(*): only import one file per line (#2470)
591a0a00
feat(mk_iff_of_inductive_prop): add, use, and document command (#2490)
2fb6022e
chore(scripts): update nolints.txt (#2494)
691a230f
chore(tactic/apply_fun): add doc string and remove duplication (#2485)
bcbdebaa
chore(scripts): update nolints.txt (#2495)
4dadd26d
feat(category_theory): wide pullbacks and limits in the over category…
4d94de48
feat(category_theory/epi_mono): opposite epi mono properties (#2479)
7c10fd2b
chore(tactic/suggest): add a docstring (#2499)
8a7b94fb
chore(*): remove unnecessary transitive imports (#2496)
64e464f1
feat(data/string): add phrasings common to conventional languages (#2…
9ccfa926
feat(data/string): add docstrings and improve semantics (#2497)
fc7ac675
doc(tactic/*): doc entries for some missing tactics (#2489)
fdbf22d7
chore(scripts): update nolints.txt (#2503)
01967486
feat(cmd/simp): let `#simp` use declared `variables` (#2478)
02d73084
feat(algebra): define `invertible` typeclass (#2504)
b7af2838
chore(tactic/pi_instance): add a docstring, remove a little bit of re…
e7bd3127
feat(linear_algebra): quadratic forms (#2480)
3ae22de4
chore(data/list/*): various renamings to use dot notation (#2481)
13393e3c
docs(*): merge rewrite tactic tag into rewriting (#2512)
00d7da20
chore(tactic/*): remove some unused args in commands (#2498)
c8946c9d
chore(*): add missing copyright headers (#2505)
62feebc2
chore(topology/algebra/module): make `id` use explicit args (#2509)
7a718662
chore(scripts): update nolints.txt (#2510)
2f6b8d73
feat(tactic/delta_instance): protect names and deal with functions (#…
3162c1c9
chore(scripts): update nolints.txt (#2514)
6795c9df
feat(data/list): more lemmas on joins and sums (#2501)
ee8451b9
chore(topology/separation): prove that `{y | y ≠ x}` is open (#2506)
3e54e977
refactor(zmod): merge `zmodp` into `zmod`, use `[fact p.prime]` for t…
e918f726
chore(scripts): update nolints.txt (#2515)
22d89c40
chore(scripts): update nolints.txt (#2517)
06f8c556
refactor(tactic/suggest): call library_search and suggest with additi…
199f6fe4
feat(order/filter/bases): add `exists_iff` and `forall_iff` (#2507)
3c8584d6
chore(*): move quadratic_reciprocity to number_theory/ (#2520)
f192f2fe
refactor(*): use [fact p.prime] for frobenius and perfect_closure (#2…
2b955327
refactor(geometry/manifold/real_instances): use fact instead of lt_cl…
d9327e43
feat(continued_fractions) add equivalence of convergents computations…
632c4baa
refactor(data/padics/*): use [fact p.prime] to assume that p is prime…
94fd41a2
feat(data/bool): add de Morgan's laws (#2523)
a8ae8e8e
doc(algebra/order_functions): add docstring and lemma (#2526)
ba4dc1a4
doc(data/nat/modeq): add module docstring and lemma (#2528)
5219ca1a
chore(algebra/module): use bundled homs for `smul_sum` and `sum_smul`…
ee6f20a6
chore(data/option,order/bounded_lattice): 2 simple lemmas about `get_…
bda206ab
chore(scripts): update nolints.txt (#2537)
c34add7a
refactor(tactic/nth_rewrite): enable rewriting hypotheses, add docstr…
1182e910
feat(analysis/normed_space/basic): add continuous_at.div (#2532)
401d3216
chore(data/real/ennreal): +2 simple lemmas (#2539)
21d8e0af
feat(data/nat/basic): add `iterate_one` and `iterate_mul` (#2540)
21b72922
feat(analysis/calculus/deriv): define `has_strict_deriv_at` (#2524)
11ccc1b5
feat(topology/algebra/module): ker, range, cod_restrict, subtype_val,…
40e97d37
chore(data/finset): add `coe_map`, `coe_image_subset_range`, and `coe…
c170ce3a
feat(measure_theory/measure_space): pigeonhole principle in a measure…
74b96471
chore(scripts): update nolints.txt (#2541)
30ae5ba2
chore(scripts): update nolints.txt (#2542)
fa13d160
doc(field_theory/subfield): don't mention unbundled homs in the comme…
942b795c
chore(ring_theory/adjoin_root): drop `is_ring_hom` instance (#2546)
039c5a6d
chore(scripts): update nolints.txt (#2548)
134c5a52
chore(data/real/*): use bundled homs to prove `coe_sum` etc (#2533)
2fc9b158
chore(topology/algebra/module): don't use unbundled homs for `algebra…
948d0fff
chore(ring_theory/algebra): move instances about complex to get rid o…
fd3afb44
feat(category_theory/concrete): make constructing morphisms easier (#…
ae06db33
fix(tactic/doc_commands): clean up copy_doc_string command (#2543)
9c818865
feat(data/complex/basic): inv_I and div_I (#2550)
f5679628
feat(data/fin): add some lemmas about coercions (#2522)
f6c93723
chore(data/dfinsupp): use more precise `decidable` requirement (#2535)
3c02800d
feat(analysis/calculus/inverse): Inverse function theorem (#2228)
c435b1cb
chore(category): rename to control (#2516)
d12db89a
chore(scripts): update nolints.txt (#2555)
94ff59ad
doc(install/*): remove outdated youtube links (#2559)
ba9fc4d7
chore(category_theory): remove `[𝒞 : category.{v₁} C] / include 𝒞` (#…
cb3a017f
chore(algebra/*): missing `simp`/`inj` lemmas (#2557)
f8fe5968
chore(data/nat/basic): move `iterate_inj` to `injective.iterate` (#2561)
84f8b395
feat(field_theory/subfield): is_subfield.inter and is_subfield.Inter …
45800696
refactor(analysis/complex/exponential): define log x = log |x| for x…
8490c545
chore(data/equiv/ring): make ring_aut reducible (#2563)
e6491de7
refactor(analysis/complex/exponential): split into three files in spe…
b14a26ee
fix(tactic/interactive): make `inhabit` work on quantified goals (#2570)
9c8bc7a5
doc(.github): remove pull-request template (#2568)
ee70afbe
refactor(tsum): use ∑' instead of ∑ as notation (#2571)
8fa8f175
feat(*): small additions that prepare for Chevalley-Warning (#2560)
caf93b74
chore(scripts): update nolints.txt (#2572)
06adf7d1
fix(scripts): stop updating mathlib-nightly repository (#2576)
c568bb40
feat(data/mv_polynomial): lemmas on total_degree (#2575)
d3140fbe
feat(topology/instances/real_vector_space): `E →+ F` to `E →L[ℝ] F` (…
74d24aba
feat(algebra/group_ring_action) define group actions on rings (#2566)
67f3fdea
fix(tactic/lint/basic): remove default argument for auto_decl and ena…
ee488b27
chore(algebra/group_with_zero): rename div_eq_inv_mul' to div_eq_inv_…
6a2559a5
feat(algebra/lie_algebra): define simple Lie algebras and define clas…
4daa7e8f
chore(group_theory/perm): delete duplicate lemmas (#2584)
eb383b14
doc(tactic/rcases): mention the "rfl" pattern (#2585)
d0a1d776
feat(algebra/group_ring_action): action on polynomials (#2586)
738bbae0
feat(order/bounded_lattice): introduce `is_compl` predicate (#2569)
9d57f682
fix(data/int/basic): use has_coe_t to prevent looping (#2573)
06bae3e1
feat(*): several `@[simp]` lemmas (#2579)
b902f6e0
chore(algebra/ordered_field): move inv_neg to field and prove for div…
1cc83e9c
refactor(algebra/big_operators): introduce notation for finset.prod a…
a99f9b55
chore(build.yml): Don't build nolints branch (#2591)
d1eae214
chore(*): switch to lean 3.10.0 (#2587)
a223bbb6
chore(scripts): update nolints.txt (#2593)
08a17d62
feat(algebra/big_operators): prod_comp (#2594)
70245f43
feat(combinatorics/composition): refactor compositions, split a list …
14aa1f7b
feat(ring_theory/ideals): quotient map to residue field as ring hom (…
1c4b5ec9
feat(algebra/midpoint): define `midpoint`, prove basic properties (#2…
d6ddfd2f
feat(data/polynomial): misc on derivatives of polynomials (#2596)
91b39066
feat(algebra/char_p): add lemma ring_char_ne_one (#2595)
7a367f37
feat(group_theory/order_of_element): order_of_eq_prime (#2604)
0c1b60b6
chore(field_theory/finite): meaningful variable names (#2606)
a66d0a81
refactor(*): remove instance max depth (#2608)
359031f9
feat(data/equiv/basic): some elementary equivs (#2602)
0db59dbf
refactor(field_theory): move finite_card.lean into finite.lean (#2607)
c7593cc5
chore(scripts): update nolints.txt (#2610)
4503f8fe
feat(*): lemmas on sums and products over fintypes (#2598)
55931556
chore(data/pnat/basic): add `mk_le_mk`, `mk_lt_mk`, `coe_le_coe`, `co…
93a64dae
feat(algebra/units): some norm_cast attributes (#2612)
0a7ff10f
feat(analysis/analytic/composition): the composition of formal series…
b1c0398a
refactor(data/equiv/local_equiv, topology/local_homeomorph): use coer…
460d9d43
chore(*): a few missing `simp` lemmas (#2615)
c3d76d01
chore(data/set/countable): use dot syntax here and there (#2617)
0c8d2e28
chore(scripts): update nolints.txt (#2621)
a8eafb65
chore(scripts): update nolints.txt (#2622)
f6edebaa
chore(data/set/basic): use implicit args in `set.ext_iff` (#2619)
a6415d79
feat(*): define `equiv.reflection` and `isometry.reflection` (#2609)
da10afcf
feat(algebra/lie_algebra): `lie_algebra.of_associative_algebra` is fu…
6c484441
refactor(order/lattice): add `sup/inf_eq_*`, rename `inf_le_inf_*` (#…
5d3b8307
chore(linear_algebra/basic): review (#2616)
bdce1956
chore(data/polynomial): remove unused argument (#2626)
ed453c72
feat(data/equiv/encodable): `ulower` lowers countable types to `Type …
a7e80393
chore(scripts): update nolints.txt (#2628)
ac3fb4eb
chore(`analysis/normed_space/banach`): minor review (#2631)
fc8c4b9f
feat(src/ring_theory/algebra): define equivalence of algebras (#2625)
67e19cd9
feat(data/nat/cast): nat.cast_with_bot (#2636)
96efc220
feat(data/nat/basic): add `mod_add_mod` and `add_mod_mod` (#2635)
e1192f35
chore(data/finset): drop `to_set`, use `has_lift` instead (#2629)
20c74188
feat(tactic/norm_num): new all-lean norm_num (#2589)
b7698468
refactor(computability/turing_machine): add list_blank (#2605)
08d43163
chore(logic/embedding,order/order_iso): review (#2618)
d04429fa
feat(algebra/ordered_*): arithmetic operations on monotone functions …
9f33b7dd
chore(scripts): update nolints.txt (#2642)
a584d527
chore(*): move to lean-3.11.0 (#2632)
81f97bdf
chore(scripts): update nolints.txt (#2643)
75900904
chore(algebra/char_zero): add `∀ n : ℕ, (n + 1 : α) ≠ 0` (#2644)
b248481b
feat(meta/uchange): universe lifting and lowering in meta (#2627)
3710744b
fix(library_search): use custom apply tactic for the main goal, as we…
8c6b14ea
feat(*): prove some `*.iterate` theorems (#2647)
b9bdc678
refactor(data/fintype/basic): weaken assumptions of set.fintype (#2650)
7146082c
feat(algebra/ring): monoid structure on `R →+* R` (#2649)
ff37fb8a
refactor(data/real/pi): add tactics for pi computation (#2641)
e777d0b4
chore(scripts): update nolints.txt (#2653)
a87f326d
test(tactic/norm_num): import tests from lean core (#2654)
eb9e3824
feat(data/list): assorted lemmas (#2651)
8c887216
chore(scripts): update nolints.txt (#2662)
f0e78172
feat(ring_theory/integral_domain): sum in integral domain indexed by …
295b87ec
fix(order/filter/basic): markdown error in module doc (#2664)
61b59ec5
feat(number_theory/basic): dvd_sub_pow_of_dvd_sub (#2640)
3f216bc6
feat(analysis/normed_space): add Mazur-Ulam theorem (#2214)
ff184e6d
chore(topology/instances/ennreal): add +1 version of `tsum_eq_supr_su…
77b3d504
chore(*): unify use of left and right for injectivity lemmas (#2655)
34a0c8c5
feat(data/matrix): matrix and vector notation (#2656)
11415339
feat(category_theory/creates): creates limits => preserves limits (#2…
437fdaf8
feat(analysis/specific_limits): more geometric series (#2658)
cbffb34c
feat(topology/bounded_continuous_function): the normed space C^0 (#2660)
4857284a
feat(topology/separation): add `subtype.t1_space` and `subtype.regula…
51e2b4cc
chore(group_theory/submonoid): use `complete_lattice_of_Inf` (#2661)
ed183f95
feat(analysis/calculus/(f)deriv): differentiability of a finite sum o…
ce86d33b
feat(category_theory): preadditive categories (#2663)
506a71f9
chore(scripts): update nolints.txt (#2669)
c9f2cbcd
feat(topology/algebra/infinite_sum): sums on subtypes (#2659)
9f16f866
refactor(scripts/mk_all): generate a single deterministic all.lean fi…
fc0c0258
refactor(order/lattice): adjust proofs to avoid choice (#2666)
f7cb3634
chore(algebra/free_monoid): add a custom `rec_on` (#2670)
6ffb6137
chore(logic/function): move to `logic/function/basic` (#2677)
7077b588
doc(*): move most docs to website, update links (#2676)
d0beb496
chore(linear_algebra/basis): use dot notation, simplify some proofs (…
3da777aa
chore(logic/function): drop `function.uncurry'` (#2678)
2871bd1e
chore(scripts): update nolints.txt (#2679)
03c272e5
chore(algebra/ring): lemmas about units in a semiring (#2680)
d412cfd0
feat(topology): a few properties of `tendsto _ _ (𝓤 α)` (#2645)
7427f8e0
perf(tactic/ext): NEVER USE `user_attribute.get_param` (#2674)
606be81d
chore(scripts): update nolints.txt (#2682)
be03a3d4
feat(data/nat/choose): Sum a row of Pascal's triangle (#2684)
378aa0d7
feat(category_theory/limits/lattice): finite limits in a semilattice …
f07ac364
chore(data/int/basic): mark cast_sub with simp attribute (#2687)
b44fa3ca
perf(tactic/ring): use new norm_num, avoid mk_app (#2685)
471d29e8
chore(scripts): update nolints.txt (#2690)
a4266a01
fix(tactic/norm_num): div/mod with negative first arg (#2689)
14a82b30
feat(analysis/special_functions/exp_log): power series for log around…
f5f7a3cf
chore(*): bump to lean-3.12.0 (#2681)
1b85e3c2
feat(category_theory/limits/shapes): avoid choice for binary products…
74286f51
doc(tactic/solve_by_elim): improve docs (#2696)
4b71428d
Fix merge conflict
acc4b7ac
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Milestone
No milestone
Login to write a write a comment.
Login via GitHub