Make prime-avoidance branch build #4925
Ms2ger
merged
3196 commits into
leanprover-community:prime-avoidance
from
prime-avoidance
feat(topology/sheaves): an equivalent sheaf condition (#4538)
25d83437
feat(archive/imo): variant solution to IMO 1962 problem 4 (#4640)
b145c36f
feat(ring_theory/polynomial/content): definition of content + proof t…
688157f8
feat(algebra/algebra/subalgebra): subalgebra.subsingleton (#4631)
82ff1e56
feat(algebra/algebra/basic): product of two algebras (#4632)
85eb12df
feat(finsupp/basic): Add a variant of `prod_map_domain_index` for whe…
edddb3b2
feat(algebra/gcd_monoid, polynomial/field_division): generalizing `no…
6e5b6cc0
chore(algebra/*): add a few `prod.*` instances (#4659)
589ebf59
chore(linear_algebra/affine_space): redefine `line_map`, add `to_affi…
0b9afe18
chore(group/type_tags): Add missing simp lemmas (#4651)
03674679
refactor(algebra/quadratic_discriminant): drop linearity condition; c…
95d33ee9
feat(archive/imo): add IMO 2019 problem 4 (#4482)
c83c28a1
feat(algebra/group_power): Add mul/add variants of powers_hom and fri…
e83458cb
feat(measure_theory/measure_space): added sub for measure_theory.meas…
13cd192e
fix(solve_by_elim): handle multiple goals with different hypotheses (…
b977dbac
feat(logic/nontrivial): make `nontriviality` work for more goals (#4574)
ebd2b7f2
chore(data/finsupp/basic): rename type variables (#4624)
f9908388
chore(order/filter): add a few lemmas (#4661)
95852107
chore(data/set/intervals): more lemmas (#4662)
77dc6794
chore(scripts): update nolints.txt (#4665)
c7782bb1
feat(measure_theory/prod): product measures and Fubini's theorem (#4590)
db06b677
chore(analysis/normed_space/basic): add `continuous_at.inv'`, `contin…
cc32876d
feat(topology/subset_properties): define `filter.cocompact` (#4666)
e21dc7a9
chore(analysis/calculus/fderiv): golf a lemma using new `nontrivialit…
fee2dfaa
feat(analysis/special_functions/trigonometric): range_{exp,cos,sin} (…
93b7e635
chore(order/filter): run `dsimp only [set.mem_set_of_eq]` in `filter_…
392d52c2
chore(order/filter): use implicit arguments in `tendsto_at_top` etc (…
4faf2e21
chore(linear_algebra/affine_space): introduce notation for `affine_ma…
61e1111d
fix(logic/nontrivial): change tactic doc entry tag to more common "ty…
1ac5d822
refactor(tactic/norm_num): define prove_ne_zero using prove_ne (#4626)
49bb5dd9
fix(data/equiv): nolint typo (#4677)
9d1bbd10
chore(scripts): update nolints.txt (#4680)
d174295c
feat(*): make int.nonneg irreducible (#4601)
4b890a24
feat(ring_theory/adjoin): adjoin_singleton_one (#4633)
7601a7a5
feat(algebra/infinite_sum): make tsum irreducible (#4679)
41c227a1
feat(algebra/*): some simp lemmas, and changing binders (#4681)
f75dbd3d
feat(ring_theory/polynomial/chebyshev): chebyshev polynomials of the …
c38d128c
feat(data/complex/exponential): bounds on exp (#4432)
47dcecd2
feat(linear_algebra/matrix): multiplying `is_basis.to_matrix` and `l…
ef9d00f7
feat(algebra/ordered_semiring): relax 0 < 1 to 0 ≤ 1 (#4363)
4140f789
feat(ring_theory/witt_vector/structure_polynomial): examples and basi…
0f1bc68f
fix(tactic/norm_num): remove unnecessary argument to rat.cast_zero (#…
cacc297c
chore(data/multiset): add a few lemmas
45caa4f3
Revert "chore(data/multiset): add a few lemmas"
a1f17706
chore(logic/function): `simp`lify applications of `(un)curry` (#4696)
0523b61d
feat(data/monoid_algebra): add missing has_coe_to_fun (#4315)
5065471e
feat(archive/imo): formalize IMO 1998 problem 2 (#4502)
a249c9a4
feat(tactic/unify_equations): add unify_equations tactic (#4515)
0c70cf30
feat(data/polynomial/reverse): define `reverse f`, prove that `revers…
006b2e70
feat({field,ring}_theory/adjoin): generalize `induction_on_adjoin` (#…
30195815
chore(topology/instances/ennreal): prove `nnreal.not_summable_iff_ten…
86d65f8d
doc(algebra/algebra/basic): Fixes some documentation about `R`-algebr…
cc6594a5
feat(algebra/free_algebra): Add a ring instance (#4692)
b3003023
refactor(ring_theory/witt_vector): move lemmas to separate file (#4693)
b707e989
chore(data/multiset): add a few lemmas (#4697)
706b4841
chore(data/finsupp): `to_additive` on `on_finset_sum` (#4698)
accc50ed
chore(scripts): update nolints.txt (#4704)
9755ae3c
feat(measure_theory): finite_spanning_sets_in (#4668)
cd884eb8
feat(data/real/pi): Leibniz's series for pi (#4228)
050b5a1b
chore(data/set): a few more lemmas about `image2` (#4695)
0cf8a98b
chore(topology/algebra/ordered): drop section vars, golf 2 proofs (#4…
21415c8c
chore(data/polynomial): slightly generalize `map_eq_zero` and `map_ne…
288802b6
chore(data/finsupp): minor review (#4712)
b46190f9
feat(linear_algebra/affine_space/ordered): define `slope` (#4669)
617e8295
fix(tactic/norm_num): remove one_div from simp set (#4705)
8131349c
chore(.gitignore): gitignore for emacs temp files (#4699)
5d52ea42
chore(*): review some lemmas about injectivity of coercions (#4711)
cf551ee3
feat(data/complex/module): ![1, I] is a basis of C over R (#4713)
8489972a
chore(category_theory/limits/preserves): split up files and remove re…
857cbd52
fixup(category_theory/sites): add arrow sets that aren't sieves (#4703)
3a860cc4
chore(scripts): update nolints.txt (#4721)
01c1e6fb
chore(linear_algebra/basic): a few simp lemmas (#4727)
75316cad
feat(linear_algebra/affine_space): define `affine_equiv` (#2909)
1b4e7694
feat(archive): formalize compiler correctness by McCarthy and Painter…
df450024
chore(scripts): update nolints.txt (#4730)
fca876ea
feat(algebra/gcd_monoid): noncomputably defines `gcd_monoid` structur…
4c4d47c2
refactor(algebra/add_torsor): define pointwise `-ᵥ` and `+ᵥ` on sets …
03f0285d
feat(linear_algebra/nonsingular_inverse): state Cramer's rule explici…
fb5ef2b9
feat(algebra/monoid_algebra): define a non-commutative version of `li…
aba31c93
chore(*): 3 unrelated small changes (#4732)
add50960
chore(data/equiv/basic): Add a simp lemma perm.coe_mul (#4723)
6eb55641
chore(data/polynomial): remove monomial_one_eq_X_pow (#4734)
de12036b
chore(scripts): update nolints.txt (#4747)
8bd1df59
feat(category_theory/yoneda): better simp lemmas for small yoneda (#4…
f2793132
feat(measure_theory/measure_space): Added lemmas for commuting restri…
ff711a31
refactor(*): lmul is an algebra hom (#4724)
dc4ad812
feat(linear_algebra/basic): define `linear_equiv.neg` (#4749)
bb52355b
chore(algebra/group/basic): Mark inv_involutive simp (#4744)
458c833e
chore(topology/*): add two missing simp coe lemmas (#4748)
468c01c8
feat(linear_algebra/affine_space): define `affine_equiv.mk'` (#4750)
9e4ef854
feat(ring_theory/witt_vector/defs): type of witt vectors + ring opera…
04b55727
feat(analysis/p_series): prove the p-series convergence test (#4360)
278a14b3
feat(ring_theory/roots_of_unity): Roots of unity as union of primitiv…
82b4843c
refactor(*): use is_scalar_tower instead of restrict_scalars (#4733)
70b14cee
fix(deprecated/*): remove instances (#4735)
fb4aee0d
feat(tactic/core): add `run_parser` user command (#4745)
b651c6f6
feat(data/{nat,list}/basic): Add some trivial lemmas (#4738)
58869614
fix(deprecated/group): Correct the name of `is_add_group_hom has_neg.…
0bbf3e29
chore(*): a few more type-specific ext lemmas (#4741)
5afeb9b9
feat(category_theory): presheaf is colimit of representables (#4401)
aa590397
feat(algebra/direct_sum): Bundle the homomorphisms (#4754)
4ec88dbe
feat(data/list/basic): Add prod_reverse_noncomm (#4757)
c141eed8
feat(data/pnat/basic): Add strong induction on pnat (#4736)
8255507e
fix(tactic/core): use eval_pexpr in run_parser_cmd (#4761)
2987a496
feat(linear_algebra/nonsingular_inverse): add stronger form of Cramer…
b9a94d69
feat(data/polynomial/ring_division): Two easy lemmas about polynomial…
570c293a
feat(ring_theory/polynomial/content): `gcd_monoid` instance on polyno…
de6a9d41
feat(algebra/direct_sum): Fix two todos about generalizing over uniqu…
cae77dc7
chore(analysis/normed_space): add 2 `@[simp]` attrs (#4775)
f056468f
chore(algebra/group/pi): add `pi.has_div` (#4776)
14cff9ac
chore(ring_theory/unique_factorization_domain): fix some lemma names …
69f550cb
chore(linear_algebra/tensor_product): missing simp lemmas (#4769)
151f0dd2
fix(tactic/core): fix infinite loop in emit_code_here (#4746)
e7a4b12c
feat(analysis/normed_space/add_torsor): continuity of `vadd`/`vsub` (…
a9d3ce8e
feat(algebra/big_operators/nat_antidiagonal): a few more lemmas (#4783)
40362122
chore(data/polynomial/{degree/basic, eval}): Some trivial lemmas abou…
6e4fe98c
chore(algebra/group/hom): use `coe_comp` in `simp` lemmas (#4780)
121c9a49
chore(order/galois_connection): define `with_bot.gi_get_or_else_bot` …
b2b39edd
chore(scripts): update nolints.txt (#4785)
7be82f94
feat(ring_theory/witt_vector/basic): verifying the ring axioms (#4694)
2e90c600
feat(data/dfinsupp): Add missing to_additive lemmas (#4788)
ba5594a6
feat(simps): improve error messages (#4653)
83edb506
chore(algebra/module,linear_algebra): split off a `linear_map` file (…
61c095f2
feat(ring_theory/finiteness): some finiteness notions in commutative …
877a20e3
feat(tactic/rcases): add `rintro (x y : t)` support (#4722)
94285983
fix(tactic/derive_fintype): add support for props (#4777)
95b3add2
feat(degree/basic.lean): degree_lt_iff_coeff_zero (#4792)
c76c3c5c
feat(data/equiv/basic): equiv.set.powerset (#4790)
8746f083
chore(*): reflow some long lines (#4794)
6e2980ce
chore(scripts): update nolints.txt (#4797)
69db7a33
refactor(*): drop `decidable_linear_order`, switch to Lean 3.22.0 (#4…
e0b153b2
feat(tactic/simps): user-provided names for projections (#4663)
a027a37b
feat(category_theory/sites): pretopology (#4648)
99acfda0
feat(algebra/monoid_algebra): formula for `lift_nc f g (c • φ)` (#4782)
40e514cb
feat(data/vector2): add lemma map_id (#4799)
1efbf13a
feat(data/finset/lattice,order/basic): add lemmas in order_dual, prov…
a1ab984c
refactor(data/polynomial): use `linear_map` for `monomial`, review `d…
97065dbf
chore(ring_theory/fractional_ideal): change exists_eq_span_singleton_…
51e12c00
feat(data/vector2): scanl and associated lemmas (#4613)
2a7e2158
feat(algebra/algebra/subalgebra): algebra equalizer (#4791)
c7379968
chore(scripts): update nolints.txt (#4808)
4d1da548
chore(linear_algebra/affine_space/basic): split (#4767)
7807f3d3
refactor(order/filter): make `filter.has_mem semireducible (#4807)
6dfa952c
feat(analysis/special_functions/trigonometric): simp attributes for t…
216cbc49
feat(ring_theory/valuation): ring of integers (#4729)
e8f8de67
feat(equiv/basic): use @[simps] (#4652)
40da087f
feat(archive/imo): formalize IMO 1981 problem Q3 (#4599)
dfa85b54
feat(category_theory/limits/presheaf): free cocompletion (#4740)
25df2671
feat(ring_theory/unique_factorization_domain): a `normalization_monoi…
28cc74f8
feat(algebra/monoid_algebra): Bundle lift_nc_mul and lift_nc_one into…
7a37dd4e
chore(data/dfinsupp): Make some lemma arguments explicit (#4803)
80ffad0c
feat(topology/algebra/group_with_zero): introduce `has_continuous_inv…
d75da1a2
feat(tactic/dependencies): add tactics to compute (reverse) dependenc…
69d41da5
chore(scripts): update nolints.txt (#4814)
d9c82152
feat(category_theory/Fintype): Adds the category of finite types and …
1baf7017
feat(linear_algebra/finite_dimensional): finite dimensional algebra_h…
d510a637
feat(data/dfinsupp): Relax requirements of semimodule conversion to a…
8b858d0b
chore(category_theory/sites): nicer names (#4816)
7d7e850b
feat(category_theory/functor_category): monos in the functor category…
f83468d3
feat(algebra/direct_sum*): relax a lot of constraints to add_comm_mon…
d709ed6f
feat(algebra/monoid_algebra): Add an equivalence between `add_monoid_…
4d19191e
refactor(*): `midpoint`, `point_reflection`, and Mazur-Ulam in affine…
ccc98d0a
chore(data/equiv/basic): arrow_congr preserves properties of binary o…
856381c1
feat(ring_theory/unique_factorization_domain): `unique_factorization_…
78811e0a
feat(category_theory/limits/pullbacks): pullback self is id iff mono …
92af9fa8
feat(category_theory/sites): Grothendieck topology on a space (#4819)
2c7efdfc
feat(tactic/norm_num): make norm_num extensible (#4820)
fc307f9b
chore(scripts): update nolints.txt (#4825)
f510728a
feat(analysis/asymptotics): Equivalent definitions for `is_[oO] u v l…
581b2af3
feat(*): a, switch to lean 3.23 (#4802)
4003b3ee
refactor(module/ordered): make ordered_semimodule a mixin (#4719)
63c0dac6
chore(data/dfinsupp): Provide dfinsupp with a semimodule instance (#4…
072cfc55
chore(topology/basic): the set of cluster pts of a filter is a closed…
d46d0c27
feat(data/equiv, algebra/*): Add simps projections to many equivs and…
5ae192eb
feat(data/dfinsupp): Port over the `finsupp.lift_add_hom` API (#4821)
03a477c4
feat(data/polynomial): ext lemmas for homomorphisms from `polynomial …
6ec7aece
feat(field_theory/intermediate_field): equalities from inclusions and…
3aac0287
feat(ring_theory/witt_vector/is_poly): supporting ghost calculations …
d28e3d10
feat(number_theory/fermat4): The n=4 case of fermat (#4720)
58f8817e
feat(algebra, logic): Pi instances for nontrivial and monoid_with_zer…
bfadf057
feat(data/polynomial/lifts): polynomials that lift (#4796)
cc7f06bd
chore(scripts): update nolints.txt (#4844)
d5650a7f
feat(analysis/calculus/times_cont_diff): differentiability of field i…
94fa9058
chore(order/filter/bases): golf a proof (#4834)
2283cf06
feat(data/prod): comp_map (#4826)
0f39d7ad
feat(ring_theory/polynomial/basic): prerequisites for galois_definiti…
517f0b5c
feat(category_theory/sites): generate lemmas (#4840)
6fc35175
feat(algebra/module/ordered): add pi instance (#4847)
f5fd2186
feat(order/conditionally_complete_lattice): nested intervals lemma (#…
1521da68
feat(analysis/normed_space/add_torsor): distance to midpoint (#4849)
67c2b5a0
feat(data/dfinsupp): Add dfinsupp.single_eq_single_iff, and subtype.h…
17697a60
feat(data/dfinsupp): Port `finsupp.lsum` and lemmas about `lift_add_h…
3b2c97f9
refactor(data/pnat): move data.pnat.prime (#4839)
6a449305
feat(linear_algebra/affine_space/affine_map): add `affine_map.proj` (…
1f616214
chore(linear_algebra/affine_space/ordered): compare endpoints to midp…
7756265e
chore(data/finset/basic): a few lemmas about `finset.piecewise` (#4852)
f9c8abe3
refactor(order/filter): move some proofs to `bases` (#3478)
e14c3782
chore(algebra/ordered_group): use implicit args, add `add_eq_coe` (#4…
9a03bdf1
chore(group_theory/group_action): introduce `smul_comm_class` (#4770)
d91c8785
feat(category_theory/sites): functor inclusion constructions (#4845)
be161d11
refactor(tactic/norm_num): move norm_num extensions (#4822)
51cbb836
docs(order/complete_lattice): make two docstrings more detailed (#4859)
6f7c5394
chore(scripts): update nolints.txt (#4860)
7a624b88
doc(*): work around markdown2 bug for now (#4842)
4aa087aa
chore(scripts): update nolints.txt (#4868)
7c8868d8
fix(tactic/simpa): reflect more simp errors (#4865)
ecdc3197
feat(ring_theory/polynomial/content): monic polynomials are primitive…
556079b4
refactor(data/list/basic,...): more explicit args (#4866)
309df10a
chore(order/basic): move `strict_mono_coe`to `subtype` NS (#4870)
0aa6aed9
feat(algebra/algebra/subalgebra): subalgebras, when seen as submodule…
6587e840
chore({data,linear_algebra}/dfinsupp): Move linear_algebra stuff to i…
13a104d9
chore(data/fintype/card): add a few lemmas (#4877)
5334f48b
chore(data/finsupp/basic): Remove finsupp.leval which duplicates fins…
dae87bcd
chore(scripts): typo in yaml_check (#4881)
0e4f8f41
chore(scripts): update nolints.txt (#4884)
57ee2162
feat(linear_algebra/matrix): `det (reindex e e A) = det A` (#4875)
c2b6220c
feat(algebra/operations): add three lemmas (#4864)
52756281
feat(category_theory/limits/shapes/products): pi comparison morphism …
b26fc59f
chore(category_theory/limits): Use `lim_map` over `lim.map` (#4856)
63d109fe
feat(*/multilinear): define `(continuous_)multilinear_map.restrict_sc…
9851a886
chore(data/set/intervals/ord_connected): make it more useful as a typ…
34c3668e
feat(category_theory/limits/types): explicit description of equalizer…
918e28ca
feat(tactic/mk_iff_of_inductive_prop): mk_iff attribute (#4863)
4f8c490f
fix(tactic/interactive): issue where long term tooltips break layout …
6bed7d4f
feat(category_theory/limits/types): ext iff lemma (#4883)
b37d4a3d
feat(*): assorted prereqs for cyclotomic polynomials (#4887)
e88a5bb5
chore(algebra/lie): adjoint rep of lie algebra uses lowercase `ad` (#…
712a0b75
feat(order): countable categoricity of dense linear orders (#2860)
505097f4
feat(category_theory/yoneda): type level yoneda equivalence (#4889)
23a2767d
chore(scripts): update nolints.txt (#4898)
16e38718
feat(data/quaternion): define quaternions and prove some basic proper…
7ab3ca85
feat(order/filter/at_top_bot): lemmas about `map/comap` of `at_top`/`…
d88042c1
feat(data/equiv): exists unique congr (#4890)
e1d60fda
feat(category_theory/closed/cartesian): product preserves colimits (#…
7d6f37dc
feat(category_theory/limits/cones): map_cone and postcompose lemmas (…
b7991c0a
feat(analysis/calculus/times_cont_diff): add `restrict_scalars` (#4899)
beb6831f
chore(analysis/calculus/times_cont_diff): a few missing lemmas (#4900)
08770779
chore(data/finset): add a few lemmas (#4901)
6f72c228
feat(linear_algebra/tensor_product): tensoring linear maps with modul…
e303a7d9
feat(ring_theory/algebraic): if `L / K` is algebraic, then the subalg…
0081a5a4
feat(logic/basic): forall2_congr lemmas (#4904)
211b0c05
feat(ring_theory/witt_vector/teichmuller): Teichmuller representative…
5a61ef19
chore(data/W): rename `W` to `W_type` (#4909)
189063b1
chore(scripts): update nolints.txt (#4910)
834d491d
chore(topology/metric_space): more `norm_cast` lemmas, golf proofs (#…
2f07ff21
chore(algebra/module/linear_map): Derive linear_map from mul_action_h…
6a1ce57b
feat(category_theory/limits/presheaf): left adjoint if preserves coli…
40245977
feat(category_theory/limits): Any small complete category is a preord…
246df99f
Merge branch 'master' into prime-avoidance
b2ce3caf
Fix
6fc26861
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-author
Milestone
No milestone
Login to write a write a comment.
Login via GitHub