leanprover-community/mathlib

Pull Requests Commits

YaelDillies committed 3 years ago

880189cf

Merge remote-tracking branch 'origin/master' into convexity_modulus

YaelDillies committed 3 years ago

392be38c

chore(algebra/algebra/spectrum): generalize some spectrum results from `alg_hom` to `alg_hom_class` (#16177)

j-loreaux committed 3 years ago

6f1ad825

feat(topology/metric_space): Add first countability instances (#15942)

mcdoll committed 3 years ago

cf9eb049

feat(category_theory): functors preserving epis and kernels are exact (#16129)

javra committed 3 years ago

e919421b

feat(topology/algebra/module/character_space): add facts about `character_space.union_zero` (#16209)

j-loreaux committed 3 years ago

02128fe4

feat(analysis/special_functions/trigonometric): add `real.abs_sinh` (#16211)

urkud committed 3 years ago

f089486a

feat(analysis/special_functions/complex/arg): relation to `real.angle.to_real` (#16205)

jsm28 committed 3 years ago

f399d3a3

chore(algebra/algebra/basic): some helper lemmas for linear maps over algebras (#16200)

eric-wieser committed 3 years ago

0abbdc08

chore(*): golfs with rsufficesI (#16197)

ericrbg committed 3 years ago

9bc7dfa6

feat(data/rat/cast): add lemmas, golf (#16194)

urkud committed 3 years ago

aeb7facf

feat(group_theory/subgroup/basic): Add `map_is_commutative` and `comap_injective_is_commutative` (#16109)

tb65536 committed 3 years ago

62ac221e

chore(set_theory/surreal/basic): remove unnecessary namespace prefixes (#14585)

alreadydone committed 3 years ago

fadfe79b

chore(order/conditionally_complete_lattice): golf three proofs (#16064)

Ruben-VandeVelde committed 3 years ago

c205fe15

feat(analysis/special_functions/trigonometric/angle): `pi_ne_zero` (#16203)

jsm28 committed 3 years ago

0ac6ba04

feat(data/finset/lattice): four lemmas about non-membership and max/min (#16192)

adomani committed 3 years ago

40213d84

fix(topology/continuous_function/basic): use `old_structure_cmd` to define `continuous_map_class` (#16164)

dupuisf committed 3 years ago

26d0a538

feat(topology/algebra/module/character_space): provide instances of `continuous_linear_map_class`, `non_unital_alg_hom_class` and `alg_hom_class` (#16178)

j-loreaux committed 3 years ago

8f9efd68

feat(number_theory/legendre_symbol/quadratic_reciprocity): switch to Gauss sum proof, clean-up (#16171)

MichaelStollBayreuth committed 3 years ago

abb635ff

feat(analysis/special_functions/trigonometric/angle): `to_real` (#16007)

jsm28 committed 3 years ago

fa6e0243

refactor(algebra/lie): replace local instance with type synonym (#16154)

Vierkantor committed 3 years ago

841ac1a3

feat(algebra/star/self_adjoint): add `star_mul_self`, `mul_star_self` and `star_hom_apply` (#16193)

j-loreaux committed 3 years ago

0a31295e

feat(group_theory/free_group): norm of elements (#15503)

kisonecat committed 3 years ago

00eb6910

feat(list/basic): list.subset_singleton_iff (#16183)

ericrbg committed 3 years ago

4970a17c

chore(algebra/order/monoid): move lemmas (#16176)

urkud committed 3 years ago

cf7b16a6

feat(data/rat/cast): drop an unneeded typeclass assumption (#15972)

urkud committed 3 years ago

6a5a2b13

feat(data/sym/basic): add nil coe lemma (#16181)

pimotte committed 3 years ago

07052296

feat(algebra/order/ring): generalize some `mono` lemmas, use them (#14691)

urkud committed 3 years ago

bfd28571

feat(*): rsuffices golfs (#16159)

ericrbg committed 3 years ago

6155d435

refactor(analysis/convex/basic): Redefine convexity in terms of star-convexity (#16173)

YaelDillies committed 3 years ago

0da54467

Older