Skip to content

9h: lift ricci_symm to explicit g via (hg : g = hm.metric) hypothesis

7cea282
Select commit
Loading
Failed to load commit list.
Merged

9h (part 1): lift remaining RiemannCurvature theorems to explicit g #42

9h: lift ricci_symm to explicit g via (hg : g = hm.metric) hypothesis
7cea282
Select commit
Loading
Failed to load commit list.

Select a check to view from the sidebar