leanprover-community/mathlib3

Pull Requests Commits

feat(algebra/star/self_adjoint): module instance on self-adjoint elements of a star algebra (#11322)

dupuisf committed 4 years ago

ce62dbc3

feat(data/finset/basic): strengthen `finset.nonempty.cons_induction` (#11452)

eric-wieser committed 4 years ago

0d1d4c95

chore(algebra/group_power/basic): collect together ring lemmas (#11446)

eric-wieser committed 4 years ago

ff19c951

refactor(analysis/inner_product_space/basic): generalize `orthogonal_family` from submodules to maps (#11254)

hrmacbeth committed 4 years ago

df2d70d6

feat(topology/algebra/uniform_group): Condition for uniform convergence (#11391)

tb65536 committed 4 years ago

fa41b7aa

feat(algebraic_geometry): More lemmas about affine schemes and basic open sets (#11449)

erdOne committed 4 years ago

323e388c

feat(topology/separation): generalize two lemmas (#11454)

fpvandoorn committed 4 years ago

f770d6ef

feat(data/nat/totient): `totient_even` (#11436)

ericrbg committed 4 years ago

d54375ea

feat(data/finsupp/basic): add `finset_sum_apply` and `coe_fn_add_hom` (#11423)

stuart-presnell committed 4 years ago

49079c14

chore(analysis/calculus/{deriv,mean_value}): use `slope` (#11419)

urkud committed 4 years ago

757eaf4f

feat(analysis/seminorm): `semilattice_sup` on seminorms and lemmas about `ball` (#11329)

mcdoll committed 4 years ago

653fe45e

Docs typo in set_theory/cardinal: Wrong type product symbol (#11453)

nomeata committed 4 years ago

2ce607e4

chore(analysis/inner_product_space/projection): Speedup `linear_isometry_equiv.reflections_generate_dim_aux` (#11443)

eric-wieser committed 4 years ago

d8aed79b

feat(algebra/field/basic): `div_neg_self`, `neg_div_self` (#11438)

jsm28 committed 4 years ago

22a9f2eb

chore(algebra/char_p): ring_char.eq is better in the other direction, with instances, and explicit arguments (#11439)

jcommelin committed 4 years ago

201aeaa3

feat(algebraic_geometry): Gluing morphisms from an open cover. (#11441)

erdOne committed 4 years ago

011a5998

chore(analysis/complex/circle): add to_units and golf (#11435)

eric-wieser committed 4 years ago

44351a9f

feat(data/matrix/notation): relax typeclass assumptions (#11429)

madvorak committed 4 years ago

38eb719f

feat(ring_theory/discriminant): add discr_mul_is_integral_mem_adjoin (#11396)

riccardobrasca committed 4 years ago

a8618391

feat(algebraic_geometry/open_immersion): Operations on open covers. (#11442)

erdOne committed 4 years ago

5a6c13bc

feat(algebra/ne_zero): `pos_of_ne_zero_coe` (#11437)

ericrbg committed 4 years ago

e2860129

feat(analysis/normed_space/linear_isometry): coercion injectivity lemmas and add_monoid_hom_class (#11434)

eric-wieser committed 4 years ago

021baaee

feat(topology): some improvements (#11424)

fpvandoorn committed 4 years ago

61054f70

feat(combinatorics/configuration): Define the order of a projective plane (#11430)

tb65536 committed 4 years ago

3c1740ac

feat(topology/subset_properties): some compactness properties (#11425)

fpvandoorn committed 4 years ago

5a3abca1

feat(algebraic_geometry): lemmas about basic opens in schemes (#11393)

erdOne committed 4 years ago

feaf6f5e

feat(data/{multiset,finset}/sum): Disjoint sum of multisets/finsets (#11355)

YaelDillies committed 4 years ago

85accb8a

feat(analysis/inner_product_space/l2): Inner product space structure on `l2` (#11315)

hrmacbeth committed 4 years ago

9a949936

fix(algebra/star/basic): redefine `star_ordered_ring` (#11213)

dupuisf committed 4 years ago

fb2b1a01

feat(tactic/lint): include linter name in github output (#11413)

robertylewis committed 4 years ago

60c77d49

Newer Older