Commits leanprover-community/mathlib

feat(analysis/special_functions/pow): tendsto rpow lemma for ennreals (#11475)

kex-y committed 3 years ago

4ed73168

chore(data/complex/basic): add of_real_eq_one (#11496)

eric-wieser committed 3 years ago

2c2338e7

feat(analysis/special_functions/complex/arg): `arg_conj`, `arg_inv` lemmas (#11479)

jsm28 committed 3 years ago

1f6bbf9e

feat(analysis/special_functions/trigonometric/angle): more 2π = 0 lemmas (#11482)

jsm28 committed 3 years ago

f4b93c8c

feat(number_field): notation for 𝓞 K, an algebra & ∈ 𝓞 K iff (#11476)

ericrbg committed 3 years ago

ed57bdd3

feat(order/filter/ultrafilter): add some comap_inf_principal lemmas (#11495)

berndlosert committed 3 years ago

5f5bcd85

feat(algebra/star/unitary): (re)define unitary elements of a star monoid (#11457)

dupuisf committed 3 years ago

d7f8f580

feat(analysis/calculus/dslope): define dslope (#11432)

urkud committed 3 years ago

1d1f3841

chore(*): Put `simp` attribute before `to_additive` (#11488)

YaelDillies committed 3 years ago

1aee8a8d

refactor(analysis/normed_space): merge `normed_space` and `semi_normed_space` (#8218)

eric-wieser committed 3 years ago

02a4775a

feat(analysis/seminorm): Add `has_add` and `has_scalar nnreal` (#11414)

mcdoll committed 3 years ago

d60541cc

feat(algebra/star/basic): change `star_ring_aut` (notably, complex conjugation) from `ring_equiv` to `ring_hom` and make type argument explicit (#11418)

hrmacbeth committed 3 years ago

3fb5b82e

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

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