leanprover-community/mathlib

Pull Requests Commits

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

chore(analysis/inner_product_space): move `is_symmetric` to a new file lower in the import tree (#16106)

ADedecker committed 3 years ago

90bc9579

feat(data/set/prod): decidable mem instance on set prod (#16107)

dtumad committed 3 years ago

175a0959

feat(algebra/*): Algebraic instances on `lex`/`order_dual` (#16122)

YaelDillies committed 3 years ago

e0b2fa6d

refactor(data/int/cast): Use hom classes (#16024)

YaelDillies committed 3 years ago

972aa423

chore(scripts): update nolints.txt (#16179)

leanprover-community-bot committed 3 years ago

b46c8953

chore(algebra/big_operators/pi): rename `w` to `H` in assumptions (#16166)

urkud committed 3 years ago

ec73f6e3

feat(group_theory/coset): Right cosets are orbits (#16119)

tb65536 committed 3 years ago

aac3141e

feat(set_theory/cardinal/finite): `nat.card (zmod n) = n` (#16118)

tb65536 committed 3 years ago

eaeb4583

feat(algebraic_topology): split simplicial objects (#16072)

joelriou committed 3 years ago

df967907

feat(algebra/order/complete_field): generalize ring_hom_monotone (#16147)

alreadydone committed 3 years ago

ee261437

Newer Older