leanprover-community/mathlib3

Pull Requests Commits

yuma-mizuno committed 3 years ago

8818d797

Create free.lean

yuma-mizuno committed 4 years ago

def14466

feat(measure_theory/integral): weaker assumptions on Ioi integrability (#11090)

b-mehta committed 4 years ago

1a29adc4

feat(data/pnat/basic): `succ_nat_pred` (#11455)

ericrbg committed 4 years ago

1f266d62

feat(data/set/basic): add singleton_injective (#11464)

nomeata committed 4 years ago

0b4f07f1

feat(measure_theory/integral/set_to_l1): monotonicity properties of set_to_fun (#10714)

RemyDegenne committed 4 years ago

37cf695a

feat(analysis/special_functions/trigonometric/angle): `neg_coe_pi` (#11460)

jsm28 committed 4 years ago

51c5a40e

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

Older