Commits leanprover-community/mathlib3

feat(algebraic_geometry/limits): Empty scheme is initial. (#16086)

erdOne committed 3 years ago

7f06271e

feat(algebra/order/floor): `floor`/`ceil` are preserved under order ring homs (#16025)

YaelDillies committed 3 years ago

fa0bbc79

refactor(algebraic_geometry/*): Make `LocallyRingedSpace.hom` a custom structure. (#15973)

erdOne committed 3 years ago

a9402e0a

feat(ring_theory/localization/away): finitely presented as R[X]/(rX-1) (#12455)

alreadydone committed 3 years ago

94f13c65

chore(algebra/order/with_zero): Move unrelated lemmas (#15676)

YaelDillies committed 3 years ago

44de64f1

feat(analysis/complex/arg): `same_ray_iff_arg_div_eq_zero` (#16218)

jsm28 committed 3 years ago

6cc2de23

feat(data/seq/seq): prove `seq.ext` earlier (#15830)

vihdzp committed 3 years ago

757e73c5

feat(group_theory/index): `card_dvd_of_surjective` (#16133)

tb65536 committed 3 years ago

04763f32

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