leanprover-community/mathlib3

Pull Requests Commits

Update src/algebra/group/basic.lean

eric-wieser committed 4 years ago

Verified 8b481df9

add two more lemmas

eric-wieser committed 4 years ago

bdfd0775

feat(algebra/group_power/basic): iterated multiplication is power

eric-wieser committed 4 years ago

09375bbb

feat(data/polynomial/reverse): Trailing degree is multiplicative (#6351)

tb65536 committed 4 years ago

0e519766

feat(data/nat/digits): digits injective at fixed base (#6338)

pechersky committed 4 years ago

a3d951bc

feat(algebraic_geometry/prime_spectrum): specialization order (#6286)

jcommelin committed 4 years ago

2b6dec0b

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

leanprover-community-bot committed 4 years ago

dc781774

feat(algebra/group_power/basic): `abs_lt_abs_of_sqr_lt_sqr` (#6277)

benjamindavidson committed 4 years ago

2134d0c1

feat(data/list/basic): repeat injectivity (#6337)

pechersky committed 4 years ago

b8b87559

feat(data/dfinsupp): add coe lemmas (#6343)

eric-wieser committed 4 years ago

87f8db2e

docs(undergrad.yaml): recent changes (#6313)

hrmacbeth committed 4 years ago

96ae2ad1

chore(topology/order): drop an unneeded argument (#6345)

urkud committed 4 years ago

4355d171

feat(data/list/basic): drop_eq_nil_iff_le (#6336)

pechersky committed 4 years ago

ab03ebe7

feat(topology/locally_constant): basics on locally constant functions (#6192)

jcommelin committed 4 years ago

473bb7d4

feat(measure_theory/interval_integral): add simp attribute to `integral_const` (#6334)

benjamindavidson committed 4 years ago

f470cc62

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

leanprover-community-bot committed 4 years ago

4d4c7bb9

chore(topology/bases): golf a proof (#6326)

urkud committed 4 years ago

93d17601

refactor(group_theory/free_*): remove API duplicated by lift, promote lift functions to equivs (#6311)

eric-wieser committed 4 years ago

08ea23b2

fix(algebra/group/pi): remove unnecessary add_monoid requirement from pi.single_zero (#6325)

eric-wieser committed 4 years ago

dccc5421

feat(data/equiv/basic): injective iff injective after composing with equiv (#6283)

jcommelin committed 4 years ago

f0aad503

feat(algebra/regular): define regular elements (#6282)

adomani committed 4 years ago

ee8708e4

chore(*): split lines (#6323)

Julian-Kuelshammer committed 4 years ago

1855bd59

doc(algebraic_geometry/is_open_comap_C): add reference to Stacks project (#6322)

adomani committed 4 years ago

ed55502f

feat(topology): the currying homeomorphism (#6319)

TwoFX committed 4 years ago

52e29379

doc(ring_theory/*): two module docs (#6318)

Julian-Kuelshammer committed 4 years ago

26d287cc

feat(*/pi): add lemmas about how `single` interacts with operators (#6317)

eric-wieser committed 4 years ago

c7c40a7d

chore(*): fix broken Zulip archive links (#6321)

bryangingechen committed 4 years ago

4d2dcdb5

chore(ring_theory/*): split lines (#6316)

Julian-Kuelshammer committed 4 years ago

3e381ad0

refactor(linear_algebra/pi): add `linear_map.single` to match `add_monoid_hom.single` (#6315)

eric-wieser committed 4 years ago

32b9b214

chore(data/indicator_function): add a formula for the support of `indicator` (#6314)

urkud committed 4 years ago

d483bc2c

Older