Commits leanprover-community/mathlib3

khwilson committed 3 years ago

dfbf30d1

doc(README): improve documentation on how to contribute (#13116)

Girgias committed 3 years ago

6d0984db

counterexample(counterexamples/char_p_zero_ne_char_zero.lean): `char_p R 0` and `char_zero R` need not coincide (#13080)

adomani committed 3 years ago

6368956a

feat(order/monovary): Add missing `monovary` lemmas (#13243)

MantasBaksys committed 3 years ago

83225b3d

feat(measure_theory/measure/measure_space): let measure.map work with ae_measurable functions (#13241)

sgouezel committed 3 years ago

32cc8689

feat(category_theory/shift): restricting shift functors to a subcategory (#13265)

kim-em committed 3 years ago

ef51d232

feat(ring_theory/polynomial/opposites + data/{polynomial/basic + finsupp/basic}): move `op_ring_equiv` to a new file + lemmas (#13162)

adomani committed 3 years ago

c916b64d

feat(analysis/convex/topology): improve some lemmas (#13136)

urkud committed 3 years ago

d70e26bf

feat(algebra/order/monoid_lemmas_zero_lt): port some lemmas from `algebra.order.monoid_lemmas` (#12961)

astrainfinita committed 3 years ago

208ebd4e

feat(group_theory/free_product): The ping pong lemma for free groups (#12916)

nomeata committed 3 years ago

00980d9d

feat(topology/algebra/module/character_space): Introduce the character space of an algebra (#12838)

dupuisf committed 3 years ago

dfc1b4cc

feat(field_theory/krull_topology): added fintype_alg_hom (#12777)

Sebastian-Monnet committed 3 years ago

55baab3e

feat(data/list/cycle): Define `cycle.chain` analog to `list.chain` (#12970)

vihdzp committed 3 years ago

36fceb91

feat(topology/uniform_space/uniform_convergence): add lemma `tendsto_locally_uniformly_iff_forall_tendsto` (#13201)

ocfnash committed 3 years ago

de0aea46

chore(ring_theory/polynomial/basic): Generalize `polynomial.degree_lt_equiv` to commutative rings (#13190)

linesthatinterlace committed 3 years ago

26729d6d

feat(linear_algebra/bilinear_form): generalize from is_symm to is_refl (#13181)

tinval committed 3 years ago

2ff12ea3

feat(analysis/complex/arg): link same_ray and complex.arg (#12764)

ericrbg committed 3 years ago

8b8f46e4

feat(set_theory/cofinality): Golf and extend existing results relating `cof` to `sup` and `bsup` (#12321)

vihdzp committed 3 years ago

7eff2330

feat(set_theory/{ordinal_arithmetic, fixed_points}): Next fixed point of families (#12200)

vihdzp committed 3 years ago

c2d870e2

feat(group_theory): use generic `subobject_class` lemmas (#11758)

Vierkantor committed 3 years ago

b2c707cd

feat(representation_theory/basic): basics of group representation theory (#11207)

antoinelab01 committed 3 years ago

d1338749

feat(algebra/ring/boolean_ring): Turning a Boolean algebra into a Boolean ring (#6476)

bryangingechen committed 3 years ago

3fe5c932

feat(data/set/intervals/with_bot_top): lemmas about `I??` and `with_top/bot` (#4273)

urkud committed 3 years ago

9495b8cb

feat(group_theory/solvable): Golf some proofs (#13271)

tb65536 committed 3 years ago

e4f93e6f

feat(combinatorics/simple_graph/clique): Cliques (#12982)

YaelDillies committed 3 years ago

b7f7c4aa

chore(ring_theory/roots_of_unity): generalise (#13261)

ericrbg committed 3 years ago

e690875d

feat(combinatorics/additive/salem_spencer): The sphere does not contain arithmetic progressions (#13259)

YaelDillies committed 3 years ago

38796213

feat(group_theory/coset): Fintype instance for quotient by the right relation (#13257)

tb65536 committed 3 years ago

b3a0f850

feat(algebra/algebra/*): generalise (#13252)

ericrbg committed 3 years ago

e3a8ef1c

feat(group_theory/group_action/basic): Left multiplication satisfies the `quotient_action` axiom (#13249)

tb65536 committed 3 years ago

14801617