leanprover-community/mathlib3

Pull Requests Commits

b-mehta committed 3 years ago

3d51b0c2

Merge branch 'arithmetic-function-eval-prime-pow' of https://github.com/leanprover-community/mathlib into arithmetic-function-eval-prime-pow

b-mehta committed 3 years ago

99883b71

b-mehta committed 3 years ago

8906a16a

b-mehta committed 3 years ago

9a5335aa

feat(algebra/squarefree): squarefree iff no square irreducible divisors

b-mehta committed 3 years ago

7beb7cef

finish squarefree thing

b-mehta committed 3 years ago

bd99c32a

b-mehta committed 3 years ago

7603d2fd

feat(ring_theory/norm): add is_integral_norm (#11489)

riccardobrasca committed 3 years ago

a0ff65df

feat(ring_theory/graded_algebra/basic): add a helper for construction from an alg hom (#11541)

eric-wieser committed 3 years ago

6f23973a

feat(measure_theory): generalize `null_of_locally_null` to `outer_measure`, add versions (#11535)

urkud committed 3 years ago

496a744e

feat(topology/separation): add `t1_space_tfae` (#11534)

urkud committed 3 years ago

be9a5dec

feat(data/set): two simple lemmas (#11531)

sgouezel committed 3 years ago

135a92d1

feat(algebra/lie/nilpotent): a non-trivial nilpotent Lie module has non-trivial maximal trivial submodule (#11515)

ocfnash committed 3 years ago

5bbc187e

feat(algebra/big_operators/basic): Reindexing a product with a permutation (#11344)

YaelDillies committed 3 years ago

a0da4f1f

chore(order/bounded_order): golf (#11538)

urkud committed 3 years ago

8d5caba3

feat(measure_theory): drop some `measurable_set` assumptions (#11536)

urkud committed 3 years ago

a217b9c3

chore(algebra/order/ring): move lemmas about invertible into a new file (#11511)

eric-wieser committed 3 years ago

f23c00f2

feat(data/fintype/basic): `one_lt_card_iff` and `two_lt_card_iff` (#11524)

tb65536 committed 3 years ago

01fa7f52

chore(cone_category): generalize universes (#11539)

alreadydone committed 3 years ago

e895c8fa

chore(logic/basic): Make higher `forall_congr`/`exists_congr` lemmas dependent (#11490)

YaelDillies committed 3 years ago

813a191d

chore(algebra/algebra/subalgebra): lemmas about top and injectivity (#11514)

eric-wieser committed 3 years ago

99e90364

refactor(linear_algebra/{tensor,exterior}_algebra): convert to a directory (#11513)

eric-wieser committed 3 years ago

1e4da8d5

feat(analysis/normed_space/finite_dimension): the determinant is continuous on the space of continuous linear maps (#11526)

sgouezel committed 3 years ago

5b36c868

feat(src/group_theory/nilpotent): solvable_of_nilpotent (#11512)

nomeata committed 3 years ago

40725122

feat(data/equiv/basic): add `add_equiv.to_int_linear_equiv` (#11456)

nomeata committed 3 years ago

274b5309

feat(order/filter): add two lemmas (#11519)

fpvandoorn committed 3 years ago

1fbef63a

refactor(set_theory/ordinal_arithmetic): Rename `power` to `opow` (#11279)

vihdzp committed 3 years ago

e096b99a

chore(measure_theory/integral/bochner): use set_to_fun lemmas to prove integral properties (#10717)

RemyDegenne committed 3 years ago

2a8a01bc

feat(analysis/normed_space/spectrum): an algebra homomorphism into the base field is bounded (#11494)

dupuisf committed 3 years ago

905871f4

feat(measure_theory/measure): define `ae_disjoint` (#11500)

urkud committed 3 years ago

4e313969

Older