leanprover-community/mathlib

Pull Requests Commits

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

mcdoll committed 3 years ago

cf9eb049

Extract `factorization_eq_of_lt_factorization_add`

stuart-presnell committed 3 years ago

6b77b036

Add `factorization_sub_of_lt`

stuart-presnell committed 3 years ago

1ab6c757

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

stuart-presnell committed 3 years ago

e4b3ecdc

Golf `factorization_add_of_lt`

stuart-presnell committed 3 years ago

111e6940

Add `factorization_add_min`

stuart-presnell committed 3 years ago

5b26b202

Remove `factorization_eq_zero_iff_remainder'`

stuart-presnell committed 3 years ago

719f05f5

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

First proof of `factorization_add_of_lt`

stuart-presnell committed 3 years ago

c7a5ddfc

Merge branch 'SP_factorization_eq_zero' into SP_factorization_add_sub

stuart-presnell committed 3 years ago

4d01737f

Progress on `factorization_add_of_lt`

stuart-presnell committed 3 years ago

6eb8b0e0

Start `factorization_add_of_lt`

stuart-presnell committed 3 years ago

2604198e

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

Newer Older