feat(Manifold/PartitionOfUnity): Existence of global C^n smooth section for nontrivial bundles by michaellee94 · Pull Request #24966 · leanprover-community/mathlib4

michaellee94 · 2025-05-16T23:49:04Z

Add existence of global C^n smooth section for nontrivial bundles

github-actions · 2025-05-16T23:50:15Z

PR summary 366f454f66

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Geometry.Manifold.PartitionOfUnity	2292	2300	+8 (+0.35%)

Import changes for all files

Files	Import difference
`Mathlib.Geometry.Manifold.WhitneyEmbedding`	1
3 files `Mathlib.Analysis.Calculus.Rademacher` `Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff` `Mathlib.Geometry.Manifold.PartitionOfUnity`	8

Declarations diff

+ contMDiff_totalSpace_weighted_sum_of_local_sections
+ exists_contMDiffOn_section_forall_mem_convex_of_local
+ exists_smooth_section_forall_mem_convex_of_local

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

grunweg · 2025-05-17T07:28:29Z

Thanks for your PR; it's great to see progress in differential geometry! As I said on zulip - can you use this to golf the proof of exists_contMDiffOn_forall_mem_convex_of_local, please?

michaellee94 · 2025-05-17T15:07:30Z

Thanks for taking a look, @grunweg. I've golfed exists_contMDiffOn_forall_mem_convex_of_local, should be ready for another pass.

PatrickMassot

Thanks for this contribution! And sorry about the delay.

I’ve compressed proofs a bit. Some of these compressions mostly aim at showing you some tricks that you may find interesting. I recommend studying those proofs carefully to understand those tricks.

PatrickMassot · 2025-06-18T18:35:45Z

Mathlib/Geometry/Manifold/PartitionOfUnity.lean

+      (fun x => (TotalSpace.mk x (s_loc i x) : TotalSpace F_fiber V)) (U i)) :
+    ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) n
+      (fun x => (TotalSpace.mk x (∑ᶠ (j : ι), (ρ j x) • (s_loc j x)) : TotalSpace F_fiber V)) := by
+  let s_val (x : M) : V x := ∑ᶠ (j : ι), (ρ j x) • (s_loc j x)
+  intro x₀
+  apply (Bundle.contMDiffAt_section s_val x₀).mpr
+  let e₀ := trivializationAt F_fiber V x₀
+  apply ContMDiffAt.congr_of_eventuallyEq
+  · apply ρ.contMDiffAt_finsum
+    · intro j h_x₀_in_tsupport_ρj
+      have h_slocj_smooth_at_x₀ : ContMDiffAt I (I.prod 𝓘(ℝ, F_fiber)) n
+        (fun x => (TotalSpace.mk x (s_loc j x) : TotalSpace F_fiber V)) x₀ :=
+        (h_smooth_s_loc j).contMDiffAt ((hU_isOpen j).mem_nhds (hρ_subord j h_x₀_in_tsupport_ρj))
+      exact (contMDiffAt_section (s_loc j) x₀).mp h_slocj_smooth_at_x₀
+  · have : (fun x ↦ (e₀ ⟨x, s_val x⟩).2)
+            =ᶠ[𝓝 x₀]
+          fun x ↦ ∑ᶠ i, ρ i x • (e₀ ⟨x, s_loc i x⟩).2 := by
+      have h_base : {x : M | x ∈ e₀.baseSet} ∈ (𝓝 x₀) :=
+        e₀.open_baseSet.mem_nhds (FiberBundle.mem_baseSet_trivializationAt' x₀)
+      filter_upwards [ρ.eventually_fintsupport_subset x₀, h_base] with x _ hx_base
+      have hlin : IsLinearMap ℝ (fun y ↦ (e₀ ⟨x, y⟩).2) := e₀.linear ℝ hx_base
+      have hfin : {i : ι | (ρ i x • s_loc i x) ≠ 0}.Finite := by
+        refine (ρ.locallyFinite.point_finite x).subset fun i hi_smul_ne_zero => ?_
+        contrapose! hi_smul_ne_zero
+        simp only [ne_eq, smul_eq_zero, not_or, mem_setOf_eq, not_and, not_not]
+        exact fun a ↦ False.elim (hi_smul_ne_zero a)
+      let Llin : V x →ₗ[ℝ] F_fiber :=
+        { toFun    := fun y ↦ (e₀ ⟨x, y⟩).2
+          map_add' := by intro u v; simpa using hlin.map_add u v
+          map_smul' := by intro c u; simpa using hlin.map_smul c u }
+      have h_map :
+          (fun y ↦ (e₀ ⟨x, y⟩).2) (∑ᶠ i, ρ i x • s_loc i x) =
+            ∑ᶠ i, ρ i x • (fun y ↦ (e₀ ⟨x, y⟩).2) (s_loc i x) := by
+        simpa only [LinearMap.toAddMonoidHom_coe, map_smul] using
+          Llin.toAddMonoidHom.map_finsum hfin
+      exact h_map
+    exact this


Suggested change

(fun x => (TotalSpace.mk x (s_loc i x) : TotalSpace F_fiber V)) (U i)) :

ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) n

(fun x => (TotalSpace.mk x (∑ᶠ (j : ι), (ρ j x) • (s_loc j x)) : TotalSpace F_fiber V)) := by

let s_val (x : M) : V x := ∑ᶠ (j : ι), (ρ j x) • (s_loc j x)

intro x₀

apply (Bundle.contMDiffAt_section s_val x₀).mpr

let e₀ := trivializationAt F_fiber V x₀

apply ContMDiffAt.congr_of_eventuallyEq

· apply ρ.contMDiffAt_finsum

· intro j h_x₀_in_tsupport_ρj

have h_slocj_smooth_at_x₀ : ContMDiffAt I (I.prod 𝓘(ℝ, F_fiber)) n

(fun x => (TotalSpace.mk x (s_loc j x) : TotalSpace F_fiber V)) x₀ :=

(h_smooth_s_loc j).contMDiffAt ((hU_isOpen j).mem_nhds (hρ_subord j h_x₀_in_tsupport_ρj))

exact (contMDiffAt_section (s_loc j) x₀).mp h_slocj_smooth_at_x₀

· have : (fun x ↦ (e₀ ⟨x, s_val x⟩).2)

=ᶠ[𝓝 x₀]

fun x ↦ ∑ᶠ i, ρ i x • (e₀ ⟨x, s_loc i x⟩).2 := by

have h_base : {x : M | x ∈ e₀.baseSet} ∈ (𝓝 x₀) :=

e₀.open_baseSet.mem_nhds (FiberBundle.mem_baseSet_trivializationAt' x₀)

filter_upwards [ρ.eventually_fintsupport_subset x₀, h_base] with x _ hx_base

have hlin : IsLinearMap ℝ (fun y ↦ (e₀ ⟨x, y⟩).2) := e₀.linear ℝ hx_base

have hfin : {i : ι | (ρ i x • s_loc i x) ≠ 0}.Finite := by

refine (ρ.locallyFinite.point_finite x).subset fun i hi_smul_ne_zero => ?_

contrapose! hi_smul_ne_zero

simp only [ne_eq, smul_eq_zero, not_or, mem_setOf_eq, not_and, not_not]

exact fun a ↦ False.elim (hi_smul_ne_zero a)

let Llin : V x →ₗ[ℝ] F_fiber :=

{ toFun := fun y ↦ (e₀ ⟨x, y⟩).2

map_add' := by intro u v; simpa using hlin.map_add u v

map_smul' := by intro c u; simpa using hlin.map_smul c u }

have h_map :

(fun y ↦ (e₀ ⟨x, y⟩).2) (∑ᶠ i, ρ i x • s_loc i x) =

∑ᶠ i, ρ i x • (fun y ↦ (e₀ ⟨x, y⟩).2) (s_loc i x) := by

simpa only [LinearMap.toAddMonoidHom_coe, map_smul] using

Llin.toAddMonoidHom.map_finsum hfin

exact h_map

exact this

(fun x ↦ (TotalSpace.mk x (s_loc i x) : TotalSpace F_fiber V)) (U i)) :

ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) n

(fun x ↦ (TotalSpace.mk x (∑ᶠ (j : ι), (ρ j x) • (s_loc j x)) : TotalSpace F_fiber V)) := by

intro x₀

apply (Bundle.contMDiffAt_section _ x₀).mpr

let e₀ := trivializationAt F_fiber V x₀

apply ContMDiffAt.congr_of_eventuallyEq

· apply ρ.contMDiffAt_finsum

· intro j hx₀

rw [← contMDiffAt_section (s_loc j)]

exact h_smooth_s_loc j |>.contMDiffAt <| (hU_isOpen j).mem_nhds <| hρ_subord j hx₀

· have h_base : {x : M | x ∈ e₀.baseSet} ∈ 𝓝 x₀ :=

e₀.open_baseSet.mem_nhds (FiberBundle.mem_baseSet_trivializationAt' x₀)

filter_upwards [ρ.eventually_fintsupport_subset x₀, h_base] with x _ hx_base

have hfin : {i : ι | (ρ i x • s_loc i x) ≠ 0}.Finite := by

refine (ρ.locallyFinite.point_finite x).subset fun i hi_smul_ne_zero => ?_

have : ρ i x ≠ 0 ∧ s_loc i x ≠ 0 := by simpa using hi_smul_ne_zero

exact this.1

simpa using e₀.linearEquivAt ℝ x hx_base |>.toAddMonoidHom.map_finsum hfin

PatrickMassot · 2025-06-18T18:50:24Z

Mathlib/Geometry/Manifold/PartitionOfUnity.lean

+          (fun x => (⟨x, s_loc x⟩ : TotalSpace F_fiber V)) U_x₀) ∧
+        (∀ y ∈ U_x₀, s_loc y ∈ t y)) :
+    ∃ s : Cₛ^n⟮I; F_fiber, V⟯, ∀ x : M, s x ∈ t x := by
+  choose U_map h_nhds s_loc h_smooth_s_loc_on_U_map h_mem_t using Hloc
+
+  -- Construct an open cover from the interiors of the given neighborhoods.
+  let U_open_cover (x : M) : Set M := interior (U_map x)
+  have hU_isOpen : ∀ x, IsOpen (U_open_cover x) := fun x ↦ isOpen_interior
+  have hU_covers_univ : univ ⊆ ⋃ x, U_open_cover x := by
+    intro x_pt _
+    simp only [mem_iUnion, mem_univ]
+    exact ⟨x_pt, mem_interior_iff_mem_nhds.mpr (h_nhds x_pt)⟩
+
+  -- Obtain a smooth partition of unity subordinate to this open cover.
+  obtain ⟨ρ, hρ_subord⟩ : ∃ ρ : SmoothPartitionOfUnity M I M univ,
+      ρ.IsSubordinate U_open_cover :=
+    SmoothPartitionOfUnity.exists_isSubordinate
+      I isClosed_univ U_open_cover hU_isOpen hU_covers_univ
+
+  -- Define the global section `s_val` by taking a weighted sum of the local sections.
+  let s_val (x : M) : V x := ∑ᶠ (j : M), (ρ j x) • (s_loc j x)
+
+  -- Prove that `s_val`, when viewed as a map to the total space, is smooth.
+  have hs_val_tot_space_smooth : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) n
+      (fun x => (TotalSpace.mk x (s_val x) : TotalSpace F_fiber V)) := by
+    apply SmoothPartitionOfUnity.contMDiff_totalSpace_weighted_sum_of_local_sections I V ρ s_loc
+      U_open_cover hU_isOpen hρ_subord
+    intro j
+    exact (h_smooth_s_loc_on_U_map j).mono interior_subset
+
+  -- Construct the smooth section and prove it lies in the convex sets `t x`.
+  refine ⟨⟨s_val, hs_val_tot_space_smooth⟩, fun x => ?_⟩
+  apply (ht_conv x).finsum_mem (fun j => ρ.nonneg j x) (ρ.sum_eq_one (mem_univ x))
+  intro j h_ρjx_ne_zero
+  have h_x_in_tsupport_ρj : x ∈ tsupport (ρ j) := subset_closure (mem_support.mpr h_ρjx_ne_zero)
+  have h_x_in_Umap_j : x ∈ U_map j := interior_subset (hρ_subord j h_x_in_tsupport_ρj)
+  exact h_mem_t j x h_x_in_Umap_j


Suggested change

(fun x => (⟨x, s_loc x⟩ : TotalSpace F_fiber V)) U_x₀) ∧

(∀ y ∈ U_x₀, s_loc y ∈ t y)) :

∃ s : Cₛ^n⟮I; F_fiber, V⟯, ∀ x : M, s x ∈ t x := by

choose U_map h_nhds s_loc h_smooth_s_loc_on_U_map h_mem_t using Hloc

-- Construct an open cover from the interiors of the given neighborhoods.

let U_open_cover (x : M) : Set M := interior (U_map x)

have hU_isOpen : ∀ x, IsOpen (U_open_cover x) := fun x ↦ isOpen_interior

have hU_covers_univ : univ ⊆ ⋃ x, U_open_cover x := by

intro x_pt _

simp only [mem_iUnion, mem_univ]

exact ⟨x_pt, mem_interior_iff_mem_nhds.mpr (h_nhds x_pt)⟩

-- Obtain a smooth partition of unity subordinate to this open cover.

obtain ⟨ρ, hρ_subord⟩ : ∃ ρ : SmoothPartitionOfUnity M I M univ,

ρ.IsSubordinate U_open_cover :=

SmoothPartitionOfUnity.exists_isSubordinate

I isClosed_univ U_open_cover hU_isOpen hU_covers_univ

-- Define the global section `s_val` by taking a weighted sum of the local sections.

let s_val (x : M) : V x := ∑ᶠ (j : M), (ρ j x) • (s_loc j x)

-- Prove that `s_val`, when viewed as a map to the total space, is smooth.

have hs_val_tot_space_smooth : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) n

(fun x => (TotalSpace.mk x (s_val x) : TotalSpace F_fiber V)) := by

apply SmoothPartitionOfUnity.contMDiff_totalSpace_weighted_sum_of_local_sections I V ρ s_loc

U_open_cover hU_isOpen hρ_subord

intro j

exact (h_smooth_s_loc_on_U_map j).mono interior_subset

-- Construct the smooth section and prove it lies in the convex sets `t x`.

refine ⟨⟨s_val, hs_val_tot_space_smooth⟩, fun x => ?_⟩

apply (ht_conv x).finsum_mem (fun j => ρ.nonneg j x) (ρ.sum_eq_one (mem_univ x))

intro j h_ρjx_ne_zero

have h_x_in_tsupport_ρj : x ∈ tsupport (ρ j) := subset_closure (mem_support.mpr h_ρjx_ne_zero)

have h_x_in_Umap_j : x ∈ U_map j := interior_subset (hρ_subord j h_x_in_tsupport_ρj)

exact h_mem_t j x h_x_in_Umap_j

(fun x ↦ (⟨x, s_loc x⟩ : TotalSpace F_fiber V)) U_x₀) ∧

(∀ y ∈ U_x₀, s_loc y ∈ t y)) :

∃ s : Cₛ^n⟮I; F_fiber, V⟯, ∀ x : M, s x ∈ t x := by

choose W h_nhds s_loc s_smooth h_mem_t using Hloc

-- Construct an open cover from the interiors of the given neighborhoods.

let U (x : M) : Set M := interior (W x)

have U_op : ∀ x, IsOpen (U x) := fun x ↦ isOpen_interior

have hU_covers_univ : univ ⊆ ⋃ x, U x := by

intro x_pt _

simp only [mem_iUnion, mem_univ]

exact ⟨x_pt, mem_interior_iff_mem_nhds.mpr (h_nhds x_pt)⟩

-- Obtain a smooth partition of unity subordinate to this open cover.

obtain ⟨ρ, hρU⟩ : ∃ ρ : SmoothPartitionOfUnity M I M univ,

ρ.IsSubordinate U :=

SmoothPartitionOfUnity.exists_isSubordinate

I isClosed_univ U U_op hU_covers_univ

-- Define the global section `s` by taking a weighted sum of the local sections.

let s x : V x := ∑ᶠ j, (ρ j x) • s_loc j x

-- Prove that `s`, when viewed as a map to the total space, is smooth.

have s_smooth : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) n

(fun x ↦ (TotalSpace.mk x (s x) : TotalSpace F_fiber V)) :=

ρ.contMDiff_weighted_sum I V s_loc U U_op hρU fun j ↦ (s_smooth j).mono interior_subset

-- Construct the smooth section and prove it lies in the convex sets `t x`.

refine ⟨⟨s, s_smooth⟩, fun x ↦ ?_⟩

apply (ht_conv x).finsum_mem (ρ.nonneg · x) (ρ.sum_eq_one (mem_univ x))

intro j h_ρjx_ne_zero

have h_x_in_tsupport_ρj : x ∈ tsupport (ρ j) := subset_closure (mem_support.mpr h_ρjx_ne_zero)

have h_x_in_Umap_j : x ∈ W j := interior_subset (hρU j h_x_in_tsupport_ρj)

exact h_mem_t j x h_x_in_Umap_j

PatrickMassot · 2025-06-18T18:58:15Z

Mathlib/Geometry/Manifold/PartitionOfUnity.lean

 `exists_smooth_forall_mem_convex_of_local_const`. -/
 theorem exists_contMDiffOn_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t x))
    (Hloc : ∀ x : M, ∃ U ∈ 𝓝 x, ∃ g : M → F, ContMDiffOn I 𝓘(ℝ, F) n g U ∧ ∀ y ∈ U, g y ∈ t y) :
    ∃ g : C^n⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x := by


Suggested change

∃ g : C^n⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x := by

∃ g : C^n⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x :=

PatrickMassot · 2025-06-18T18:59:15Z

Mathlib/Geometry/Manifold/PartitionOfUnity.lean

+  let V (_ : M) : Type _ := F
+  rcases exists_contMDiffOn_section_forall_mem_convex_of_local I V t ht
+    (fun x₀ ↦ by
+      rcases Hloc x₀ with ⟨U, hU, g, hgs, hgt⟩
+      refine ⟨U, hU, g, ?_, hgt⟩
+      intro y hy
+      rw [@Bundle.contMDiffWithinAt_section]
+      apply hgs y hy)
+    with ⟨s, hs⟩
+  refine ⟨⟨fun x ↦ (s x : F), fun x₀ ↦ ?_⟩, hs⟩
+  have := s.contMDiff x₀
+  rw [Bundle.contMDiffAt_section] at this
+  exact this


Suggested change

let V (_ : M) : Type _ := F

rcases exists_contMDiffOn_section_forall_mem_convex_of_local I V t ht

(fun x₀ ↦ by

rcases Hloc x₀ with ⟨U, hU, g, hgs, hgt⟩

refine ⟨U, hU, g, ?_, hgt⟩

intro y hy

rw [@Bundle.contMDiffWithinAt_section]

apply hgs y hy)

with ⟨s, hs⟩

refine ⟨⟨fun x ↦ (s x : F), fun x₀ ↦ ?_⟩, hs⟩

have := s.contMDiff x₀

rw [Bundle.contMDiffAt_section] at this

exact this

let ⟨s, hs⟩ := exists_contMDiffOn_section_forall_mem_convex_of_local I (fun _ ↦ F) t ht

(fun x₀ ↦ let ⟨U, hU, g, hgs, hgt⟩ := Hloc x₀

⟨U, hU, g, fun y hy ↦ Bundle.contMDiffWithinAt_section _ _ _ |>.mpr <| hgs y hy, hgt⟩)

⟨⟨s, (Bundle.contMDiffAt_section _ _ |>.mp <| s.contMDiff ·)⟩, hs⟩

Note that such extreme golfs are meant to convey the message “this result is a direct consequence of previously proven things”.

grunweg · 2025-07-07T15:36:30Z

Hi @michaellee94! Thanks again for your PR, this will be a great addition to mathlib.
I'm visiting @PatrickMassot until next week, and we are making a lot of progress in differential geometry --- more precisely, Riemannian manifolds. One of the currently missing pieces is the existence of a Riemannian metric on a manifold, which requires this PR. It would really help to have this PR merged by e.g. Friday morning.
Do you have some time in the next days to incorporate these comments? Do you mind if I do it, otherwise?

michaellee94 · 2025-07-07T15:43:12Z

Hi, @grunweg and @PatrickMassot. Thanks for the reminder about this. Will address comments today!

michaellee94 · 2025-07-07T17:17:26Z

Continued by #26875

add existence of global C^n smooth section for nontrivial bundles

d675989

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label May 16, 2025

github-actions bot added the t-differential-geometry Manifolds etc label May 16, 2025

remove unused haves

367368d

michaellee94 requested review from PatrickMassot and grunweg May 17, 2025 00:08

michaellee94 added 2 commits May 16, 2025 23:34

let's actually pull this result out

a8f4320

replace with simp only here

2025fc6

grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label May 17, 2025

michaellee94 added 2 commits May 17, 2025 10:47

redo proof of exists_contMDiffOn_forall_mem_convex_of_local

ed2c6d3

golf it further

4311018

michaellee94 removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 17, 2025

michaellee94 added 5 commits May 17, 2025 11:10

let's fix the nomenclature here

7a76c1b

whoops, missed this one

35d9cb7

missed this as well

4f19811

typo here

f573880

Merge branch 'master' into michaellee94/smooth_section

366f454

grunweg assigned PatrickMassot Jun 18, 2025

PatrickMassot reviewed Jun 18, 2025

View reviewed changes

PatrickMassot added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 18, 2025

michaellee94 mentioned this pull request Jul 7, 2025

[Merged by Bors] - feat(Manifold/PartitionOfUnity): existence of global C^n smooth section for nontrivial bundles #26875

Closed

1 task

michaellee94 closed this Jul 7, 2025

YaelDillies deleted the michaellee94/smooth_section branch August 18, 2025 07:35

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(Manifold/PartitionOfUnity): Existence of global C^n smooth section for nontrivial bundles#24966

feat(Manifold/PartitionOfUnity): Existence of global C^n smooth section for nontrivial bundles#24966
michaellee94 wants to merge 11 commits intomasterfrom
michaellee94/smooth_section

michaellee94 commented May 16, 2025

Uh oh!

github-actions bot commented May 16, 2025 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

grunweg commented May 17, 2025

Uh oh!

michaellee94 commented May 17, 2025

Uh oh!

PatrickMassot left a comment

Uh oh!

PatrickMassot Jun 18, 2025

Uh oh!

PatrickMassot Jun 18, 2025

Uh oh!

PatrickMassot Jun 18, 2025

Uh oh!

PatrickMassot Jun 18, 2025

Uh oh!

grunweg commented Jul 7, 2025 •

edited

Loading

Uh oh!

michaellee94 commented Jul 7, 2025

Uh oh!

michaellee94 commented Jul 7, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

	∃ g : C^n⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x := by
	∃ g : C^n⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x :=

Conversation

michaellee94 commented May 16, 2025

Uh oh!

github-actions bot commented May 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 366f454f66

Import changes for modified files

Declarations diff

Uh oh!

grunweg commented May 17, 2025

Uh oh!

michaellee94 commented May 17, 2025

Uh oh!

PatrickMassot left a comment

Choose a reason for hiding this comment

Uh oh!

PatrickMassot Jun 18, 2025

Choose a reason for hiding this comment

Uh oh!

PatrickMassot Jun 18, 2025

Choose a reason for hiding this comment

Uh oh!

PatrickMassot Jun 18, 2025

Choose a reason for hiding this comment

Uh oh!

PatrickMassot Jun 18, 2025

Choose a reason for hiding this comment

Uh oh!

grunweg commented Jul 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

michaellee94 commented Jul 7, 2025

Uh oh!

michaellee94 commented Jul 7, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

github-actions bot commented May 16, 2025 •

edited

Loading

grunweg commented Jul 7, 2025 •

edited

Loading