leanprover-community/mathlib

Pull Requests Commits

dupuisf committed 3 years ago

497d5331

lemmas for normal operators

dupuisf committed 3 years ago

28173bb5

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

b-mehta committed 3 years ago

1a29adc4

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

ericrbg committed 3 years ago

1f266d62

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

nomeata committed 3 years ago

0b4f07f1

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

RemyDegenne committed 3 years ago

37cf695a

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

jsm28 committed 3 years ago

51c5a40e

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

dupuisf committed 3 years ago

ce62dbc3

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

eric-wieser committed 3 years ago

0d1d4c95

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

eric-wieser committed 3 years ago

ff19c951

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

hrmacbeth committed 3 years ago

df2d70d6

define normal elements

dupuisf committed 3 years ago

b7f76ea9

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

tb65536 committed 3 years ago

fa41b7aa

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

erdOne committed 3 years ago

323e388c

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

fpvandoorn committed 3 years ago

f770d6ef

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

ericrbg committed 3 years ago

d54375ea

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

stuart-presnell committed 3 years ago

49079c14

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

urkud committed 3 years ago

757eaf4f

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

mcdoll committed 3 years ago

653fe45e

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

nomeata committed 3 years ago

2ce607e4

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

eric-wieser committed 3 years ago

d8aed79b

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

jsm28 committed 3 years ago

22a9f2eb

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

jcommelin committed 3 years ago

201aeaa3

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

erdOne committed 3 years ago

011a5998

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

eric-wieser committed 3 years ago

44351a9f

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

madvorak committed 3 years ago

38eb719f

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

riccardobrasca committed 3 years ago

a8618391

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

erdOne committed 3 years ago

5a6c13bc

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

ericrbg committed 3 years ago

e2860129

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

eric-wieser committed 3 years ago

021baaee

Newer Older