leanprover-community/mathlib3

Pull Requests Commits

feat(geometry/euclidean/oriented_angle): relation to unoriented angles (#15722)

jsm28 committed 3 years ago

674505ed

feat(algebra/order/floor): `fract_one` (#15785)

jsm28 committed 3 years ago

7dcf5c3d

chore(data/zmod): make `zmod.int_cast_zmod_cast` `@[norm_cast]` (#15753)

Vierkantor committed 3 years ago

2f1b3131

feat(topology/homeomorph): Product of sets is isomorphic to product of sets (#15664)

tb65536 committed 3 years ago

1b09efe3

fix(data/polynomial/basic): remove `monomial_fun` to remove diamonds (#15778)

ericrbg committed 3 years ago

7ad184e3

Merge branch 'AD_orthogonal_hilbert_sum' into AD_trace_class_3

ADedecker committed 3 years ago

5b5a2af6

Merge branch 'AD_subordinate_hilbert_basis' into AD_trace_class_3

ADedecker committed 3 years ago

c6437d15

Unused arguments

ADedecker committed 3 years ago

3ad9537f

ADedecker committed 3 years ago

daa15566

Merge branch 'AD_subordinate_hilbert_basis' into AD_trace_class_3

ADedecker committed 3 years ago

c910a98e

ADedecker committed 3 years ago

e971af78

ADedecker committed 3 years ago

19c3fab9

Collect Hilbert bases along a Hilbert sum decomposition

ADedecker committed 3 years ago

21ef33c8

feat(order/succ_pred/basic): `a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥` and related (#15567)

vihdzp committed 3 years ago

9bb1256d

Merge remote-tracking branch 'origin/AD_is_hilbert_sum' into AD_subordinate_hilbert_basis

ADedecker committed 3 years ago

875443fd

Merge branch 'AD_lp_curry' into AD_subordinate_hilbert_basis

ADedecker committed 3 years ago

e4be6302

ADedecker committed 3 years ago

11bbcb9d

chore(ring_theory/adjoin_root): remove duplicate namespace (#15775)

ericrbg committed 3 years ago

b6fa37ed

feat(probability/density): probability of event in uniform distribution (#15678)

b-mehta committed 3 years ago

9c473c1d

feat(data/nat/factorization/basic): add lemma `prime.factorization_self` (#15767)

stuart-presnell committed 3 years ago

a2a02a30

feat(number_theory): Bertrand's postulate, slightly different approach (#8002)

BoltonBailey committed 3 years ago

7b2ae37e

feat(ring_theory/ideal/operations): A variant of `finsupp.total` for ideals. (#15460)

erdOne committed 3 years ago

5e07117c

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

leanprover-community-bot committed 3 years ago

bff2f20c

Merge branch 'AD_lp_functorial' into AD_lp_curry

ADedecker committed 3 years ago

f9e84f27

ADedecker committed 3 years ago

30df7ef0

chore(logic/function/basic): make `function.injective.decidable_eq` protected (#15759)

ADedecker committed 3 years ago

a574fbe6

ADedecker committed 3 years ago

4f4f6209

Finish renaming

ADedecker committed 3 years ago

9ff6e5a4

Update src/analysis/normed_space/lp_space.lean

ADedecker committed 3 years ago

Verified 4c25aeb0

Define`is_hilbert_sum` predicate

ADedecker committed 3 years ago

691c6557

Newer Older